Theorem stdpc5 1798

Description: An axiom scheme of standard predicate calculus that emulates Axiom 5 of [Mendelson] p. 69. The hypothesis Ⅎxφ can be thought of as emulating "x is not free in φ." With this definition, the meaning of "not free" is less restrictive than the usual textbook definition; for example x would not (for us) be free in x = x by nfequid 1678. This theorem scheme can be proved as a metatheorem of Mendelson's axiom system, even though it is slightly stronger than his Axiom 5. (Contributed by NM, 22-Sep-1993.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof shortened by Wolf Lammen, 1-Jan-2018.)

Hypothesis

Ref	Expression
stdpc5.1	⊢ Ⅎxφ

Assertion

Ref	Expression
stdpc5	⊢ (∀x(φ → ψ) → (φ → ∀xψ))

Proof of Theorem stdpc5

Step	Hyp	Ref	Expression
1		stdpc5.1	. . 3 ⊢ Ⅎxφ
2	1	19.21 1796	. 2 ⊢ (∀x(φ → ψ) ↔ (φ → ∀xψ))
3	2	biimpi 186	1 ⊢ (∀x(φ → ψ) → (φ → ∀xψ))

Syntax hints:   → wi 4  ∀wal 1540  Ⅎwnf 1544

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-ex 1542  df-nf 1545

This theorem is referenced by:  ra5  3130