ILE Home 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