Theorem expcomd 1486

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  1488  2moswapdc  2169  indifdir  3462  reupick  3490  issod  4418  poxp  6402  smores2  6465  smoiun  6472  mapxpen  7039  f1dmvrnfibi  7148  recexprlemm  7849  ltleletr  8266  fzind  9600  iccid  10165  ssfzo12bi  10476  pfxccatin12lem2  11321  swrdccat  11325  dvdsabseq  12431  divalgb  12509  cncongr1  12698  difsqpwdvds  12934  lss1d  14421  txlm  15032  blsscls2  15246  metcnpi3  15270  clwwlknonex2lem2  16318