Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  stdpc5 GIF version

Theorem stdpc5 1564
 Description: An axiom scheme of standard predicate calculus that emulates Axiom 5 of [Mendelson] p. 69. The hypothesis Ⅎ𝑥𝜑 can be thought of as emulating "𝑥 is not free in 𝜑." With this definition, the meaning of "not free" is less restrictive than the usual textbook definition; for example 𝑥 would not (for us) be free in 𝑥 = 𝑥 by nfequid 1682. 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 𝑥𝜑
Assertion
Ref Expression
stdpc5 (∀𝑥(𝜑𝜓) → (𝜑 → ∀𝑥𝜓))

Proof of Theorem stdpc5
StepHypRef Expression
1 stdpc5.1 . . 3 𝑥𝜑
2119.21 1563 . 2 (∀𝑥(𝜑𝜓) ↔ (𝜑 → ∀𝑥𝜓))
32biimpi 119 1 (∀𝑥(𝜑𝜓) → (𝜑 → ∀𝑥𝜓))
 Colors of variables: wff set class Syntax hints:   → wi 4  ∀wal 1333  Ⅎwnf 1440 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-4 1490  ax-ial 1514  ax-i5r 1515 This theorem depends on definitions:  df-bi 116  df-nf 1441 This theorem is referenced by:  sbalyz  1979  ra5  3025
 Copyright terms: Public domain W3C validator