Theorem imp_introls_fo ≪ | index | src | ≫

\imp左侧引入\fo

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

Step	Hyp	Ref	Expression
1		imp_introrevr_imp	(\fo x A \imp A) \imp (A \imp B) \imp \fo x A \imp B
2		fo_elim	\fo x A \imp A
3	1, 2	ax_mp	(A \imp B) \imp \fo x A \imp B

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3, ax_gen, ax_4, ax_5, ax_6, ax_7, ax_12)