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

Theorem expimpd 361
 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  4186  swopo  4238  reusv3  4391  ralxfrd  4393  rexxfrd  4394  nlimsucg  4491  poirr2  4942  elpreima  5550  fmptco  5597  tposfo2  6175  nnm00  6436  th3qlem1  6542  fiintim  6833  supmoti  6896  infglbti  6928  infnlbti  6929  updjud  6983  recexprlemss1l  7494  recexprlemss1u  7495  cauappcvgprlemladdru  7515  cauappcvgprlemladdrl  7516  caucvgprlemladdrl  7537  uzind  9213  ledivge1le  9570  xltnegi  9675  ixxssixx  9742  expnegzap  10385  shftlem  10647  cau3lem  10945  caubnd2  10948  climuni  11121  2clim  11129  summodclem2  11210  summodc  11211  zsumdc  11212  fsumf1o  11218  fisumss  11220  fsumcl2lem  11226  fsumadd  11234  fsummulc2  11276  prodmodclem2  11405  prodmodc  11406  zproddc  11407  fprodf1o  11416  fprodssdc  11418  dfgcd2  11772  cncongrprm  11905  eltg3  12299  tgidm  12316  tgrest  12411  tgcn  12450  lmtopcnp  12492  txbasval  12509  txcnp  12513  bldisj  12643  xblm  12659  blssps  12669  blss  12670  blssexps  12671  blssex  12672  metcnp3  12753  bj-findis  13392
 Copyright terms: Public domain W3C validator