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

Theorem expimpd 355
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 113 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32impd 251 1 (𝜑 → ((𝜓𝜒) → 𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  euotd  4072  swopo  4124  reusv3  4273  ralxfrd  4275  rexxfrd  4276  nlimsucg  4372  poirr2  4811  elpreima  5402  fmptco  5448  tposfo2  6014  nnm00  6268  th3qlem1  6374  supmoti  6667  infglbti  6699  infnlbti  6700  updjud  6752  recexprlemss1l  7173  recexprlemss1u  7174  cauappcvgprlemladdru  7194  cauappcvgprlemladdrl  7195  caucvgprlemladdrl  7216  uzind  8827  ledivge1le  9172  xltnegi  9266  ixxssixx  9289  expnegzap  9954  shftlem  10215  cau3lem  10512  caubnd2  10515  climuni  10645  2clim  10653  isummolem2  10736  isummo  10737  zisum  10738  fsumf1o  10746  fisumss  10748  fsumcl2lem  10755  fsumadd  10763  fsummulc2  10805  dfgcd2  11085  cncongrprm  11218  bj-findis  11520
  Copyright terms: Public domain W3C validator