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

Theorem impexp 254
 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 252 . 2 (((𝜑𝜓) → 𝜒) → (𝜑 → (𝜓𝜒)))
2 pm3.31 253 . 2 ((𝜑 → (𝜓𝜒)) → ((𝜑𝜓) → 𝜒))
31, 2impbii 121 1 (((𝜑𝜓) → 𝜒) ↔ (𝜑 → (𝜓𝜒)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101   ↔ wb 102 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  imp4a  335  exp4a  352  imdistan  426  pm5.3  452  pm4.87  501  nan  636  pm4.14dc  798  pm5.6dc  846  2sb6  1876  2sb6rf  1882  2exsb  1901  mor  1958  eu2  1960  moanim  1990  r2alf  2358  r3al  2383  r19.23t  2440  ceqsralt  2598  rspc2gv  2684  ralrab  2725  ralrab2  2729  euind  2751  reu2  2752  reu3  2754  rmo4  2757  reuind  2767  rmo2ilem  2875  rmo3  2877  ralss  3034  rabss  3045  raldifb  3111  unissb  3638  elintrab  3655  ssintrab  3666  dftr5  3885  repizf2lem  3942  reusv3  4220  tfi  4333  raliunxp  4505  fununi  4995  dff13  5435  dfsmo2  5933  qliftfun  6219  prime  8396  raluz  8617  raluz2  8618  ralrp  8702  facwordi  9608  bdcriota  10390
 Copyright terms: Public domain W3C validator