Theorem syldan 282

Description: A syllogism deduction with conjoined antecents. (Contributed by NM, 24-Feb-2005.) (Proof shortened by Wolf Lammen, 6-Apr-2013.)

Hypotheses

Ref	Expression
syldan.1	|- ( ( ph /\ ps ) -> ch )
syldan.2	|- ( ( ph /\ ch ) -> th )

Assertion

Ref	Expression
syldan	|- ( ( ph /\ ps ) -> th )

Proof of Theorem syldan

Step	Hyp	Ref	Expression
1		syldan.1	. 2 |- ( ( ph /\ ps ) -> ch )
2		syldan.2	. . . 4 |- ( ( ph /\ ch ) -> th )
3	2	expcom 116	. . 3 |- ( ch -> ( ph -> th ) )
4	3	adantrd 279	. 2 |- ( ch -> ( ( ph /\ ps ) -> th ) )
5	1, 4	mpcom 36	1 |- ( ( ph /\ ps ) -> th )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108

This theorem is referenced by:  sylan2  286  dn1dc  963  stoic2a  1449  sbcied2  3036  csbied2  3141  elpw2g  4200  pofun  4359  tfi  4630  fnbr  5378  caovlem2d  6139  caofcom  6189  fnexALT  6196  tfr1onlemres  6435  tfrcllemres  6448  tfri3  6453  ixpexgg  6809  f1domg  6849  fundmfi  7039  f1ofi  7045  finacn  7316  archnqq  7530  nqpru  7665  ltaddpr  7710  1idsr  7881  addgt0sr  7888  suplocsrlempr  7920  gt0ap0  8699  ap0gt0  8713  mulgt1  8936  gt0div  8943  ge0div  8944  ltdiv2  8960  creur  9032  avgle1  9278  recnz  9466  qreccl  9763  xrrege0  9947  peano2fzor  10361  flqltnz  10430  flqdiv  10466  zmodcl  10489  frecuzrdgtcl  10557  frecuzrdgfunlem  10564  seqfveqg  10623  seq3fveq  10624  ser3mono  10632  seqsplitg  10634  seqcaopr2g  10639  iseqf1olemkle  10642  seq3f1olemqsumkj  10656  seq3f1olemqsumk  10657  seqf1oglem2  10665  seqf1og  10666  seq3id  10670  seq3z  10673  seqhomog  10675  le2sq2  10760  bcpasc  10911  fihasheqf1oi  10932  seq3coll  10987  wrdnval  11024  wrdsymb1  11030  lswcl  11044  ccatlid  11062  ccatass  11064  ccat1st1st  11093  lswccats1fst  11096  swrdlsw  11122  ccatswrd  11123  caucvgrelemcau  11291  caucvgre  11292  r19.2uz  11304  sqrtgt0  11345  xrmaxiflemval  11561  clim2ser  11648  clim2ser2  11649  climub  11655  serf0  11663  fsumf1o  11701  fisumss  11703  fsumcl2lem  11709  fsumsplit  11718  fsum2dlemstep  11745  fisumrev2  11757  fsumlessfi  11771  telfsumo  11777  fsumparts  11781  fsumiun  11788  binom1dif  11798  isumsplit  11802  isumrpcl  11805  isumlessdc  11807  explecnv  11816  cvgratnnlemmn  11836  cvgratz  11843  cvgratgt0  11844  mertenslemi1  11846  clim2prod  11850  clim2divap  11851  fprodseq  11894  fprodf1o  11899  prodssdc  11900  fprodssdc  11901  fprodsplitdc  11907  fprodeq0  11928  fprod2dlemstep  11933  ef0lem  11971  eftlub  12001  tanval3ap  12025  dvdssubr  12150  divalgmod  12238  bitsdc  12258  bitsp1  12262  divgcdnn  12296  algfx  12374  eucalgcvga  12380  lcmcllem  12389  lcmneg  12396  isprm6  12469  cncongrprm  12479  phimullem  12547  pcid  12647  pcgcd  12652  pcz  12655  4sqlem9  12709  4sqlem15  12728  4sqlem16  12729  imasex  13137  grpidd  13215  gsumress  13227  ismndd  13269  subsubm  13315  grpinvid1  13384  grpinvid2  13385  grplcan  13394  grpinvinv  13399  grpinvval2  13415  mulgass  13495  mulgpropdg  13500  subginv  13517  subgmulg  13524  issubg2m  13525  issubg4m  13529  subsubg  13533  eqger  13560  qusinv  13572  resghm  13596  conjsubgen  13614  rngrz  13708  isrngd  13715  ringidss  13791  isringd  13803  ringlz  13805  ringrz  13806  unitgrp  13878  0unit  13891  unitnegcl  13892  dvrass  13901  dvreq1  13904  dvrdir  13905  ringinvdv  13907  invrpropdg  13911  rhmunitinv  13940  issubrng2  13972  subsubrng  13976  subrg1  13993  issubrg2  14003  subsubrg  14007  lmod0vs  14083  lmodvs0  14084  lmodvneg1  14092  islss3  14141  lspsnsubg  14158  lspid  14159  lspssv  14160  lspidm  14163  lspsnneg  14182  sraval  14199  qus1  14288  zringmulg  14360  mulgrhm  14371  znidom  14419  tgcl  14536  tgclb  14537  tgss2  14551  ntrss3  14595  ntridm  14598  opnssneib  14628  ssnei2  14629  innei  14635  resttopon  14643  cnpnei  14691  cnntri  14696  lmss  14718  txcnp  14743  blpnfctr  14911  mopni2  14955  bdmopn  14976  climcncf  15056  ivthdec  15116  cnplimcim  15139  dvconst  15166  dvconstre  15168  dvef  15199  plymullem  15222  plycoeid3  15229  rpcxpneg  15379  abscxp  15387  sgmmul  15468  lgscllem  15484  lgsvalmod  15496  lgsdir2  15510  lgsquadlem2  15555  lgsquad2lem2  15559  cvgcmp2nlemabs  15971  trilpolemisumle  15977  trilpolemeq1  15979  trilpolemlt1  15980  nconstwlpolemgt0  16003  neapmkvlem  16006