Theorem fo_imp_ins ≪ | index | src | ≫

\fo对\imp插入

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

Step	Hyp	Ref	Expression
1		ax_4	\fo x (A \imp B) \imp \fo x A \imp \fo x B

Axiom use

Logic (ax_4)