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

Theorem expimpd 358
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-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  euotd  4136  swopo  4188  reusv3  4341  ralxfrd  4343  rexxfrd  4344  nlimsucg  4441  poirr2  4889  elpreima  5493  fmptco  5540  tposfo2  6118  nnm00  6379  th3qlem1  6485  fiintim  6770  supmoti  6832  infglbti  6864  infnlbti  6865  updjud  6919  recexprlemss1l  7391  recexprlemss1u  7392  cauappcvgprlemladdru  7412  cauappcvgprlemladdrl  7413  caucvgprlemladdrl  7434  uzind  9066  ledivge1le  9412  xltnegi  9511  ixxssixx  9578  expnegzap  10220  shftlem  10481  cau3lem  10778  caubnd2  10781  climuni  10954  2clim  10962  summodclem2  11043  summodc  11044  zsumdc  11045  fsumf1o  11051  fisumss  11053  fsumcl2lem  11059  fsumadd  11067  fsummulc2  11109  dfgcd2  11548  cncongrprm  11681  eltg3  12069  tgidm  12086  tgrest  12181  tgcn  12219  lmtopcnp  12261  txbasval  12278  txcnp  12282  bldisj  12390  xblm  12406  blssps  12416  blss  12417  blssexps  12418  blssex  12419  metcnp3  12500  bj-findis  12869
  Copyright terms: Public domain W3C validator