Theorem fo_swap ≪ | index | src | ≫

\fo交换

theorem fo_swap {x y: set} (A: wff x y): $ \fo x \fo y A \imp \fo y \fo x A $;

Step	Hyp	Ref	Expression
1		ax_11	\fo x \fo y A \imp \fo y \fo x A

Axiom use

Logic (ax_11)