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

Theorem exlimih 1481
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 (ψxψ)
exlimih.2 (φψ)
Assertion
Ref Expression
exlimih (xφψ)

Proof of Theorem exlimih
StepHypRef Expression
1 exlimih.1 . . 3 (ψxψ)
2119.23h 1384 . 2 (x(φψ) ↔ (xφψ))
3 exlimih.2 . 2 (φψ)
42, 3mpgbi 1338 1 (xφψ)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1240  wex 1378
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-gen 1335  ax-ie2 1380
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  exlimi  1482  exlimiv  1486  19.43  1516  hbex  1524  ax6blem  1537  19.41h  1572  ax9o  1585  equid  1586  equsex  1613  cbvexh  1635  equs5a  1672  sb5rf  1729  equvin  1740  euan  1953  moexexdc  1981
  Copyright terms: Public domain W3C validator