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  3133  reupick  4292  pwssun  5530  ordelord  6354  tz7.7  6358  onelssex  6381  poxp  8107  smores2  8323  smoiun  8330  smogt  8336  tz7.49  8413  omsmolem  8621  mapxpen  9107  fodomfir  9279  f1dmvrnfibi  9292  suplub2  9412  epfrs  9684  r1sdom  9727  rankr1ai  9751  ficardom  9914  cardsdomel  9927  dfac5lem5  10080  cfsmolem  10223  cfcoflem  10225  axdc3lem2  10404  zorn2lem7  10455  genpn0  10956  reclem2pr  11001  supsrlem  11064  ltletr  11266  fzind  12632  rpneg  12985  xrltletr  13117  iccid  13351  ssfzoulel  13721  ssfzo12bi  13722  pfxccatin12lem2  14696  swrdccat  14700  repsdf2  14743  repswswrd  14749  cshwcsh2id  14794  o1rlimmul  15585  dvdsabseq  16283  divalgb  16374  bezoutlem3  16511  cncongr1  16637  ncoprmlnprm  16698  difsqpwdvds  16858  lss1d  20869  pf1ind  22242  chfacfisf  22741  chfacfisfcpmat  22742  cayleyhamilton1  22779  txlm  23535  fmfnfmlem1  23841  blsscls2  24392  metcnpi3  24434  bcmono  27188  sletr  27670  upgrewlkle2  29534  redwlk  29600  crctcshwlkn0lem5  29744  wwlksnextwrd  29827  clwwlknonex2lem2  30037  ocnel  31227  atcvat2i  32316  atcvat4i  32326  dfon2lem5  35775  cgrxfr  36043  colinearxfr  36063  hfelhf  36169  isbasisrelowllem1  37343  isbasisrelowllem2  37344  finxpreclem6  37384  seqpo  37741  atlatle  39313  cvrexchlem  39413  cvrat2  39423  cvrat4  39437  pmapjoin  39846  onfrALTlem2  44536  onfrALTlem2VD  44878  eluzge0nn0  47313  elfz2z  47316  iccpartiltu  47423  iccpartigtl  47424  iccpartlt  47425  lighneal  47612  bgoldbtbnd  47810  tgoldbach  47818  cznnring  48250  ply1mulgsumlem2  48376  itsclc0  48760