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

Theorem exlimih 1466
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 1368 . 2 (x(φψ) ↔ (xφψ))
3 exlimih.2 . 2 (φψ)
42, 3mpgbi 1321 1 (xφψ)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1226  wex 1362
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-gen 1318  ax-ie2 1364
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  exlimi  1467  exlimiv  1471  19.43  1501  hbex  1509  ax6blem  1522  19.41h  1557  ax9o  1570  equid  1571  equsex  1598  cbvexh  1620  equs5a  1657  sb5rf  1714  equvin  1725  euan  1938  moexexdc  1966
  Copyright terms: Public domain W3C validator