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 ( ∀ 𝑥 ( ∀ 𝑥 𝜑𝜓 ) → ( ∀ 𝑥 𝜑 → ∀ 𝑥 𝜓 ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 vx 𝑥
1 wph 𝜑
2 1 0 wal 𝑥 𝜑
3 wps 𝜓
4 2 3 wi ( ∀ 𝑥 𝜑𝜓 )
5 4 0 wal 𝑥 ( ∀ 𝑥 𝜑𝜓 )
6 3 0 wal 𝑥 𝜓
7 2 6 wi ( ∀ 𝑥 𝜑 → ∀ 𝑥 𝜓 )
8 5 7 wi ( ∀ 𝑥 ( ∀ 𝑥 𝜑𝜓 ) → ( ∀ 𝑥 𝜑 → ∀ 𝑥 𝜓 ) )