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  2556  reu6  2873  fun11iun  5388  poxp  6129  smoel  6197  iinerm  6501  suplub2ti  6888  infglbti  6912  infnlbti  6913  prarloclemlo  7309  peano5uzti  9166  lbzbi  9415  ssfzo12bi  10009  cau3lem  10893  summodc  11159  mertenslem2  11312  prodmodclem2  11353  alzdvds  11558  nno  11609  nn0seqcvgd  11728  lcmdvds  11766  divgcdodd  11827  cnptoprest  12417  lmss  12424  txlm  12457
  Copyright terms: Public domain W3C validator