Theorem expcomd 1491

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

Step	Hyp	Ref	Expression
1		expcomd.1	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
2	1	expd 258	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	com23 78	1 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))

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  1493  2moswapdc  2177  indifdir  3487  reupick  3517  issod  4462  poxp  6462  smores2  6559  smoiun  6566  mapxpen  7142  f1dmvrnfibi  7252  recexprlemm  7985  ltleletr  8401  fzind  9744  iccid  10310  ssfzo12bi  10626  pfxccatin12lem2  11486  swrdccat  11490  dvdsabseq  12597  divalgb  12675  cncongr1  12864  difsqpwdvds  13100  lss1d  14703  txlm  15363  blsscls2  15577  metcnpi3  15601  clwwlknonex2lem2  16662  lealltlt1  16734