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  3391  reupick  3419  issod  4316  poxp  6227  smores2  6289  smoiun  6296  mapxpen  6842  f1dmvrnfibi  6937  recexprlemm  7614  ltleletr  8029  fzind  9357  iccid  9912  ssfzo12bi  10211  dvdsabseq  11836  divalgb  11913  cncongr1  12086  difsqpwdvds  12320  txlm  13446  blsscls2  13660  metcnpi3  13684
  Copyright terms: Public domain W3C validator