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

Theorem exlimih 1500
 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 1403 . 2 (∀𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))
3 exlimih.2 . 2 (𝜑𝜓)
42, 3mpgbi 1357 1 (∃𝑥𝜑𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4  ∀wal 1257  ∃wex 1397 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-gen 1354  ax-ie2 1399 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  exlimi  1501  exlimiv  1505  19.43  1535  hbex  1543  ax6blem  1556  19.41h  1591  ax9o  1604  equid  1605  equsex  1632  cbvexh  1654  equs5a  1691  sb5rf  1748  equvin  1759  euan  1972  moexexdc  2000
 Copyright terms: Public domain W3C validator