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

Theorem expcomd 1400
Description: Deduction form of expcom 115. (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 256 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32com23 78 1 (𝜑 → (𝜒 → (𝜓𝜃)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 107
This theorem is referenced by:  simplbi2comg  1402  2moswapdc  2065  indifdir  3298  reupick  3326  issod  4201  poxp  6083  smores2  6145  smoiun  6152  mapxpen  6695  f1dmvrnfibi  6784  recexprlemm  7377  ltleletr  7766  fzind  9067  iccid  9598  ssfzo12bi  9892  dvdsabseq  11390  divalgb  11467  cncongr1  11627  txlm  12287  blsscls2  12479  metcnpi3  12503
  Copyright terms: Public domain W3C validator