Theorem imp_intro_fo ≪ | index | src | ≫

\fo对\imp引入

theorem imp_intro_fo {x: set} (A B: wff x):
  $ A \imp B $ >
  $ \fo x A \imp \fo x B $;

Step	Hyp	Ref	Expression
1		fo_imp_ins	\fo x (A \imp B) \imp \fo x A \imp \fo x B
2		hyp h	A \imp B
3	2	intro_fo	\fo x (A \imp B)
4	1, 3	ax_mp	\fo x A \imp \fo x B

Axiom use

Logic (ax_mp, ax_gen, ax_4)