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

Theorem exlimih 1529
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 1432 . 2 (∀𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
3 exlimih.2 . 2 (𝜑𝜓)
42, 3mpgbi 1386 1 (∃𝑥𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1287  wex 1426
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-gen 1383  ax-ie2 1428
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  exlimi  1530  exlimiv  1534  19.43  1564  hbex  1572  ax6blem  1585  19.41h  1620  ax9o  1633  equid  1634  equsex  1663  cbvexh  1685  equs5a  1722  sb5rf  1780  equvin  1791  euan  2004  moexexdc  2032
  Copyright terms: Public domain W3C validator