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  4038  swopo  4090  reusv3  4239  ralxfrd  4241  rexxfrd  4242  nlimsucg  4338  poirr2  4768  elpreima  5340  fmptco  5384  tposfo2  5938  nnm00  6191  th3qlem1  6297  supmoti  6502  infglbti  6534  infnlbti  6535  updjud  6577  recexprlemss1l  6964  recexprlemss1u  6965  cauappcvgprlemladdru  6985  cauappcvgprlemladdrl  6986  caucvgprlemladdrl  7007  uzind  8616  ledivge1le  8961  xltnegi  9055  ixxssixx  9078  expnegzap  9684  shftlem  9930  cau3lem  10226  caubnd2  10229  climuni  10358  2clim  10366  dfgcd2  10635  cncongrprm  10768  bj-findis  11066
 Copyright terms: Public domain W3C validator