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

Theorem expcomd 1441
Description: Deduction form of expcom 116. (Contributed by Alan Sare, 22-Jul-2012.)
Hypothesis
Ref Expression
expcomd.1 (𝜑 → ((𝜓𝜒) → 𝜃))
Assertion
Ref Expression
expcomd (𝜑 → (𝜒 → (𝜓𝜃)))

Proof of Theorem expcomd
StepHypRef Expression
1 expcomd.1 . . 3 (𝜑 → ((𝜓𝜒) → 𝜃))
21expd 258 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32com23 78 1 (𝜑 → (𝜒 → (𝜓𝜃)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108
This theorem is referenced by:  simplbi2comg  1443  2moswapdc  2116  indifdir  3393  reupick  3421  issod  4321  poxp  6235  smores2  6297  smoiun  6304  mapxpen  6850  f1dmvrnfibi  6945  recexprlemm  7625  ltleletr  8041  fzind  9370  iccid  9927  ssfzo12bi  10227  dvdsabseq  11855  divalgb  11932  cncongr1  12105  difsqpwdvds  12339  lss1d  13475  txlm  13818  blsscls2  14032  metcnpi3  14056
  Copyright terms: Public domain W3C validator