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  3129  reupick  4282  pwssun  5515  ordelord  6333  tz7.7  6337  onelssex  6360  poxp  8068  smores2  8284  smoiun  8291  smogt  8297  tz7.49  8374  omsmolem  8582  mapxpen  9067  fodomfir  9237  f1dmvrnfibi  9250  suplub2  9370  epfrs  9646  r1sdom  9689  rankr1ai  9713  ficardom  9876  cardsdomel  9889  dfac5lem5  10040  cfsmolem  10183  cfcoflem  10185  axdc3lem2  10364  zorn2lem7  10415  genpn0  10916  reclem2pr  10961  supsrlem  11024  ltletr  11226  fzind  12592  rpneg  12945  xrltletr  13077  iccid  13311  ssfzoulel  13681  ssfzo12bi  13682  pfxccatin12lem2  14655  swrdccat  14659  repsdf2  14702  repswswrd  14708  cshwcsh2id  14753  o1rlimmul  15544  dvdsabseq  16242  divalgb  16333  bezoutlem3  16470  cncongr1  16596  ncoprmlnprm  16657  difsqpwdvds  16817  lss1d  20884  pf1ind  22258  chfacfisf  22757  chfacfisfcpmat  22758  cayleyhamilton1  22795  txlm  23551  fmfnfmlem1  23857  blsscls2  24408  metcnpi3  24450  bcmono  27204  sletr  27686  upgrewlkle2  29570  redwlk  29634  crctcshwlkn0lem5  29777  wwlksnextwrd  29860  clwwlknonex2lem2  30070  ocnel  31260  atcvat2i  32349  atcvat4i  32359  dfon2lem5  35760  cgrxfr  36028  colinearxfr  36048  hfelhf  36154  isbasisrelowllem1  37328  isbasisrelowllem2  37329  finxpreclem6  37369  seqpo  37726  atlatle  39298  cvrexchlem  39398  cvrat2  39408  cvrat4  39422  pmapjoin  39831  onfrALTlem2  44520  onfrALTlem2VD  44862  eluzge0nn0  47297  elfz2z  47300  iccpartiltu  47407  iccpartigtl  47408  iccpartlt  47409  lighneal  47596  bgoldbtbnd  47794  tgoldbach  47802  cznnring  48247  ply1mulgsumlem2  48373  itsclc0  48757