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

Theorem impexp 261
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 259 . 2 (((𝜑𝜓) → 𝜒) → (𝜑 → (𝜓𝜒)))
2 pm3.31 260 . 2 ((𝜑 → (𝜓𝜒)) → ((𝜑𝜓) → 𝜒))
31, 2impbii 125 1 (((𝜑𝜓) → 𝜒) ↔ (𝜑 → (𝜓𝜒)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  imp4a  344  exp4a  361  imdistan  438  pm5.3  464  pm4.87  529  nan  664  pm4.14dc  858  pm5.6dc  894  2sb6  1935  2sb6rf  1941  2exsb  1960  mor  2017  eu2  2019  moanim  2049  r2alf  2427  r3al  2452  r19.23t  2514  ceqsralt  2685  rspc2gv  2773  ralrab  2816  ralrab2  2820  euind  2842  reu2  2843  reu3  2845  rmo4  2848  rmo3f  2852  reuind  2860  rmo2ilem  2968  rmo3  2970  ralss  3131  rabss  3142  raldifb  3184  unissb  3734  elintrab  3751  ssintrab  3762  dftr5  3997  repizf2lem  4053  reusv3  4349  tfi  4464  raliunxp  4648  fununi  5159  dff13  5635  dfsmo2  6150  tfr1onlemaccex  6211  tfrcllemaccex  6224  qliftfun  6477  prime  9101  raluz  9322  raluz2  9323  ralrp  9411  facwordi  10426  modfsummod  11167  isprm2  11694  isprm4  11696  metcnp  12576  limcdifap  12674  bdcriota  12883
  Copyright terms: Public domain W3C validator