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  4278  pwssun  5511  ordelord  6333  tz7.7  6337  onelssex  6360  poxp  8064  smores2  8280  smoiun  8287  smogt  8293  tz7.49  8370  omsmolem  8578  mapxpen  9063  fodomfir  9219  f1dmvrnfibi  9232  suplub2  9352  epfrs  9628  r1sdom  9674  rankr1ai  9698  ficardom  9861  cardsdomel  9874  dfac5lem5  10025  cfsmolem  10168  cfcoflem  10170  axdc3lem2  10349  zorn2lem7  10400  genpn0  10901  reclem2pr  10946  supsrlem  11009  ltletr  11212  fzind  12577  rpneg  12926  xrltletr  13058  iccid  13292  ssfzoulel  13662  ssfzo12bi  13663  pfxccatin12lem2  14640  swrdccat  14644  repsdf2  14687  repswswrd  14693  cshwcsh2id  14737  o1rlimmul  15528  dvdsabseq  16226  divalgb  16317  bezoutlem3  16454  cncongr1  16580  ncoprmlnprm  16641  difsqpwdvds  16801  lss1d  20898  pf1ind  22271  chfacfisf  22770  chfacfisfcpmat  22771  cayleyhamilton1  22808  txlm  23564  fmfnfmlem1  23870  blsscls2  24420  metcnpi3  24462  bcmono  27216  sletr  27698  upgrewlkle2  29587  redwlk  29651  crctcshwlkn0lem5  29794  wwlksnextwrd  29877  clwwlknonex2lem2  30090  ocnel  31280  atcvat2i  32369  atcvat4i  32379  rankfilimb  35134  trssfir1om  35143  trssfir1omregs  35153  dfon2lem5  35850  cgrxfr  36120  colinearxfr  36140  hfelhf  36246  isbasisrelowllem1  37420  isbasisrelowllem2  37421  finxpreclem6  37461  seqpo  37807  atlatle  39439  cvrexchlem  39538  cvrat2  39548  cvrat4  39562  pmapjoin  39971  onfrALTlem2  44663  onfrALTlem2VD  45005  eluzge0nn0  47436  elfz2z  47439  iccpartiltu  47546  iccpartigtl  47547  iccpartlt  47548  lighneal  47735  bgoldbtbnd  47933  tgoldbach  47941  cznnring  48386  ply1mulgsumlem2  48512  itsclc0  48896