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

Theorem exlimih 1572
 Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.)
Hypotheses
Ref Expression
exlimih.1 (𝜓 → ∀𝑥𝜓)
exlimih.2 (𝜑𝜓)
Assertion
Ref Expression
exlimih (∃𝑥𝜑𝜓)

Proof of Theorem exlimih
StepHypRef Expression
1 exlimih.1 . . 3 (𝜓 → ∀𝑥𝜓)
2119.23h 1474 . 2 (∀𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
3 exlimih.2 . 2 (𝜑𝜓)
42, 3mpgbi 1428 1 (∃𝑥𝜑𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4  ∀wal 1329  ∃wex 1468 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-gen 1425  ax-ie2 1470 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  exlimi  1573  exlimiv  1577  19.43  1607  hbex  1615  ax6blem  1628  19.41h  1663  ax9o  1676  equid  1677  equsex  1706  cbvexh  1728  equs5a  1766  sb5rf  1824  equvin  1835  euan  2055  moexexdc  2083
 Copyright terms: Public domain W3C validator