Metamath Proof Explorer


Axiom ax-c4

Description: Axiom of Quantified Implication. This axiom moves a universal quantifier from outside to inside an implication, quantifying ps . Notice that x must not be a free variable in the antecedent of the quantified implication, and we express this by binding ph to "protect" the axiom from a ph containing a free x . Axiom scheme C4' in Megill p. 448 (p. 16 of the preprint). It is a special case of Lemma 5 of Monk2 p. 108 and Axiom 5 of Mendelson p. 69.

This axiom is obsolete and should no longer be used. It is proved above as Theorem axc4 . (Contributed by NM, 3-Jan-1993) (New usage is discouraged.)

Ref Expression
Assertion ax-c4 x x φ ψ x φ x ψ

Detailed syntax breakdown

Step Hyp Ref Expression
0 vx setvar x
1 wph wff φ
2 1 0 wal wff x φ
3 wps wff ψ
4 2 3 wi wff x φ ψ
5 4 0 wal wff x x φ ψ
6 3 0 wal wff x ψ
7 2 6 wi wff x φ x ψ
8 5 7 wi wff x x φ ψ x φ x ψ