Theorem expcomd 417

Description: Deduction form of expcom 414. (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 416	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	com23 86	1 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))

Syntax hints:   → wi 4   ∧ wa 396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 208  df-an 397

This theorem is referenced by:  ancomsd  466  simplbi2comt  502  ralrimdva  3158  reupick  4213  pwssun  5351  ordelord  6095  tz7.7  6099  poxp  7682  smores2  7850  smoiun  7857  smogt  7863  tz7.49  7939  omsmolem  8137  mapxpen  8537  f1dmvrnfibi  8661  suplub2  8778  epfrs  9026  r1sdom  9056  rankr1ai  9080  ficardom  9243  cardsdomel  9256  dfac5lem5  9406  cfsmolem  9545  cfcoflem  9547  axdc3lem2  9726  zorn2lem7  9777  genpn0  10278  reclem2pr  10323  supsrlem  10386  ltletr  10585  fzind  11934  rpneg  12275  xrltletr  12404  iccid  12637  ssfzoulel  12985  ssfzo12bi  12986  pfxccatin12lem2  13933  swrdccat  13937  repsdf2  13980  repswswrd  13986  cshwcsh2id  14030  o1rlimmul  14813  dvdsabseq  15500  divalgb  15592  bezoutlem3  15722  cncongr1  15844  ncoprmlnprm  15901  difsqpwdvds  16056  lss1d  19429  pf1ind  20204  chfacfisf  21150  chfacfisfcpmat  21151  cayleyhamilton1  21188  txlm  21944  fmfnfmlem1  22250  blsscls2  22801  metcnpi3  22843  bcmono  25539  upgrewlkle2  27075  redwlk  27140  crctcshwlkn0lem5  27278  wwlksnextwrd  27361  clwwlknonex2lem2  27573  ocnel  28762  atcvat2i  29851  atcvat4i  29861  dfon2lem5  32642  sletr  32848  cgrxfr  33127  colinearxfr  33147  hfelhf  33253  isbasisrelowllem1  34188  isbasisrelowllem2  34189  finxpreclem6  34229  seqpo  34575  atlatle  36008  cvrexchlem  36107  cvrat2  36117  cvrat4  36131  pmapjoin  36540  onfrALTlem2  40440  onfrALTlem2VD  40783  eluzge0nn0  43050  elfz2z  43053  iccpartiltu  43086  iccpartigtl  43087  iccpartlt  43088  lighneal  43280  bgoldbtbnd  43478  tgoldbach  43486  cznnring  43727  ply1mulgsumlem2  43943  itsclc0  44261