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 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  simplbi2comg  1493  2moswapdc  2177  indifdir  3487  reupick  3517  issod  4464  poxp  6468  smores2  6565  smoiun  6572  mapxpen  7148  f1dmvrnfibi  7258  recexprlemm  7991  ltleletr  8407  fzind  9763  iccid  10329  ssfzo12bi  10645  pfxccatin12lem2  11505  swrdccat  11509  dvdsabseq  12616  divalgb  12694  cncongr1  12883  difsqpwdvds  13119  lss1d  14722  txlm  15382  blsscls2  15596  metcnpi3  15620  bcmono  16124  clwwlknonex2lem2  16691  lealltlt1  16763