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

Theorem expdimp 256
Description: A deduction version of exportation, followed by importation. (Contributed by NM, 6-Sep-2008.)
Hypothesis
Ref Expression
exp3a.1 (𝜑 → ((𝜓𝜒) → 𝜃))
Assertion
Ref Expression
expdimp ((𝜑𝜓) → (𝜒𝜃))

Proof of Theorem expdimp
StepHypRef Expression
1 exp3a.1 . . 3 (𝜑 → ((𝜓𝜒) → 𝜃))
21expd 255 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp 123 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:  rexlimdvv  2496  reu6  2805  fun11iun  5287  poxp  6011  smoel  6079  iinerm  6378  suplub2ti  6750  infglbti  6774  infnlbti  6775  prarloclemlo  7114  peano5uzti  8915  lbzbi  9162  ssfzo12bi  9697  cau3lem  10608  isummo  10834  mertenslem2  10991  alzdvds  11194  nno  11245  nn0seqcvgd  11362  lcmdvds  11400  divgcdodd  11461
  Copyright terms: Public domain W3C validator