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

Theorem expimpd 360
Description: Exportation followed by a deduction version of importation. (Contributed by NM, 6-Sep-2008.)
Hypothesis
Ref Expression
expimpd.1 ((𝜑𝜓) → (𝜒𝜃))
Assertion
Ref Expression
expimpd (𝜑 → ((𝜓𝜒) → 𝜃))

Proof of Theorem expimpd
StepHypRef Expression
1 expimpd.1 . . 3 ((𝜑𝜓) → (𝜒𝜃))
21ex 114 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32impd 252 1 (𝜑 → ((𝜓𝜒) → 𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
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 is referenced by:  euotd  4146  swopo  4198  reusv3  4351  ralxfrd  4353  rexxfrd  4354  nlimsucg  4451  poirr2  4901  elpreima  5507  fmptco  5554  tposfo2  6132  nnm00  6393  th3qlem1  6499  fiintim  6785  supmoti  6848  infglbti  6880  infnlbti  6881  updjud  6935  recexprlemss1l  7411  recexprlemss1u  7412  cauappcvgprlemladdru  7432  cauappcvgprlemladdrl  7433  caucvgprlemladdrl  7454  uzind  9130  ledivge1le  9481  xltnegi  9586  ixxssixx  9653  expnegzap  10295  shftlem  10556  cau3lem  10854  caubnd2  10857  climuni  11030  2clim  11038  summodclem2  11119  summodc  11120  zsumdc  11121  fsumf1o  11127  fisumss  11129  fsumcl2lem  11135  fsumadd  11143  fsummulc2  11185  dfgcd2  11629  cncongrprm  11762  eltg3  12153  tgidm  12170  tgrest  12265  tgcn  12304  lmtopcnp  12346  txbasval  12363  txcnp  12367  bldisj  12497  xblm  12513  blssps  12523  blss  12524  blssexps  12525  blssex  12526  metcnp3  12607  bj-findis  13104
  Copyright terms: Public domain W3C validator