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

Theorem expcomd 1346
Description: Deduction form of expcom 113. (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 249 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32com23 76 1 (𝜑 → (𝜒 → (𝜓𝜃)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 105
This theorem is referenced by:  simplbi2comg  1348  2moswapdc  2006  indifdir  3221  reupick  3249  trintssmOLD  3899  issod  4084  poxp  5881  smores2  5940  smoiun  5947  recexprlemm  6780  ltleletr  7159  fzind  8412  iccid  8895  ssfzo12bi  9183  dvdsabseq  10159  divalgb  10237
  Copyright terms: Public domain W3C validator