Theorem expcomd 416

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  ancomsd  465  simplbi2comt  501  ralrimdva  3160  reupick  4348  pwssun  5590  ordelord  6417  tz7.7  6421  onelssex  6443  poxp  8169  smores2  8410  smoiun  8417  smogt  8423  tz7.49  8501  omsmolem  8713  mapxpen  9209  fodomfir  9396  f1dmvrnfibi  9409  suplub2  9530  epfrs  9800  r1sdom  9843  rankr1ai  9867  ficardom  10030  cardsdomel  10043  dfac5lem5  10196  cfsmolem  10339  cfcoflem  10341  axdc3lem2  10520  zorn2lem7  10571  genpn0  11072  reclem2pr  11117  supsrlem  11180  ltletr  11382  fzind  12741  rpneg  13089  xrltletr  13219  iccid  13452  ssfzoulel  13810  ssfzo12bi  13811  pfxccatin12lem2  14779  swrdccat  14783  repsdf2  14826  repswswrd  14832  cshwcsh2id  14877  o1rlimmul  15665  dvdsabseq  16361  divalgb  16452  bezoutlem3  16588  cncongr1  16714  ncoprmlnprm  16775  difsqpwdvds  16934  lss1d  20984  pf1ind  22380  chfacfisf  22881  chfacfisfcpmat  22882  cayleyhamilton1  22919  txlm  23677  fmfnfmlem1  23983  blsscls2  24538  metcnpi3  24580  bcmono  27339  sletr  27821  upgrewlkle2  29642  redwlk  29708  crctcshwlkn0lem5  29847  wwlksnextwrd  29930  clwwlknonex2lem2  30140  ocnel  31330  atcvat2i  32419  atcvat4i  32429  dfon2lem5  35751  cgrxfr  36019  colinearxfr  36039  hfelhf  36145  isbasisrelowllem1  37321  isbasisrelowllem2  37322  finxpreclem6  37362  seqpo  37707  atlatle  39276  cvrexchlem  39376  cvrat2  39386  cvrat4  39400  pmapjoin  39809  onfrALTlem2  44517  onfrALTlem2VD  44860  eluzge0nn0  47227  elfz2z  47230  iccpartiltu  47296  iccpartigtl  47297  iccpartlt  47298  lighneal  47485  bgoldbtbnd  47683  tgoldbach  47691  cznnring  47985  ply1mulgsumlem2  48116  itsclc0  48505