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

Theorem impexp 250
 Description: Import-export theorem. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 24-Mar-2013.)
Assertion
Ref Expression
impexp (((φ ψ) → χ) ↔ (φ → (ψχ)))

Proof of Theorem impexp
StepHypRef Expression
1 pm3.3 248 . 2 (((φ ψ) → χ) → (φ → (ψχ)))
2 pm3.31 249 . 2 ((φ → (ψχ)) → ((φ ψ) → χ))
31, 2impbii 117 1 (((φ ψ) → χ) ↔ (φ → (ψχ)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  imp4a  331  exp4a  348  imdistan  418  pm5.3  444  pm4.87  493  nan  625  pm4.14dc  786  pm5.6dc  834  2sb6  1857  2sb6rf  1863  2exsb  1882  mor  1939  eu2  1941  moanim  1971  r2alf  2335  r3al  2360  r19.23t  2417  ceqsralt  2575  ralrab  2696  ralrab2  2700  euind  2722  reu2  2723  reu3  2725  rmo4  2728  reuind  2738  rmo2ilem  2841  rmo3  2843  ralss  3000  rabss  3011  raldifb  3077  unissb  3601  elintrab  3618  ssintrab  3629  dftr5  3848  repizf2lem  3905  reusv3  4158  tfi  4248  raliunxp  4420  fununi  4910  dff13  5350  dfsmo2  5843  qliftfun  6124  prime  8113  raluz  8297  raluz2  8298  ralrp  8379  bdcriota  9338
 Copyright terms: Public domain W3C validator