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  2170  indifdir  3463  reupick  3491  issod  4416  poxp  6397  smores2  6460  smoiun  6467  mapxpen  7034  f1dmvrnfibi  7143  recexprlemm  7844  ltleletr  8261  fzind  9595  iccid  10160  ssfzo12bi  10471  pfxccatin12lem2  11313  swrdccat  11317  dvdsabseq  12410  divalgb  12488  cncongr1  12677  difsqpwdvds  12913  lss1d  14400  txlm  15006  blsscls2  15220  metcnpi3  15244  clwwlknonex2lem2  16292