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
|- ( A. x ( A. x ph -> ps ) -> ( A. x ph -> A. x ps ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 vx
 |-  x
1 wph
 |-  ph
2 1 0 wal
 |-  A. x ph
3 wps
 |-  ps
4 2 3 wi
 |-  ( A. x ph -> ps )
5 4 0 wal
 |-  A. x ( A. x ph -> ps )
6 3 0 wal
 |-  A. x ps
7 2 6 wi
 |-  ( A. x ph -> A. x ps )
8 5 7 wi
 |-  ( A. x ( A. x ph -> ps ) -> ( A. x ph -> A. x ps ) )