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

Theorem expdimp 257
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 256 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp 123 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:  rexlimdvv  2594  reu6  2919  fun11iun  5463  poxp  6211  smoel  6279  iinerm  6585  suplub2ti  6978  infglbti  7002  infnlbti  7003  prarloclemlo  7456  peano5uzti  9320  lbzbi  9575  ssfzo12bi  10181  cau3lem  11078  summodc  11346  mertenslem2  11499  prodmodclem2  11540  alzdvds  11814  nno  11865  nn0seqcvgd  11995  lcmdvds  12033  divgcdodd  12097  prmpwdvds  12307  cnptoprest  13033  lmss  13040  txlm  13073
  Copyright terms: Public domain W3C validator