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

Theorem expcomd 1375
Description: Deduction form of expcom 114. (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 254 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32com23 77 1 (𝜑 → (𝜒 → (𝜓𝜃)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106
This theorem is referenced by:  simplbi2comg  1377  2moswapdc  2038  indifdir  3253  reupick  3281  trintssmOLD  3945  issod  4137  poxp  5979  smores2  6041  smoiun  6048  mapxpen  6544  f1dmvrnfibi  6632  recexprlemm  7162  ltleletr  7546  fzind  8831  iccid  9312  ssfzo12bi  9601  dvdsabseq  10930  divalgb  11007  cncongr1  11167
  Copyright terms: Public domain W3C validator