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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108

This theorem is used by:  sylan2  286  dn1dc  973  stoic2a  1478  sbcied2  3089  csbied2  3195  elpw2g  4294  pofun  4459  tfi  4731  fnbr  5488  caovlem2d  6285  caofcom  6337  fnexALT  6344  elabreximd  6360  tfr1onlemres  6625  tfrcllemres  6638  tfri3  6643  ixpexgg  7010  f1domg  7050  fundmfi  7257  f1ofi  7263  finacn  7566  archnqq  7790  nqpru  7925  ltaddpr  7970  1idsr  8141  addgt0sr  8148  suplocsrlempr  8180  gt0ap0  8962  ap0gt0  8976  mulgt1  9201  gt0div  9208  ge0div  9209  ltdiv2  9225  creur  9297  avgle1  9557  recnz  9749  qreccl  10057  xrrege0  10243  peano2fzor  10666  flqltnz  10742  flqdiv  10778  zmodcl  10801  frecuzrdgtcl  10869  frecuzrdgfunlem  10876  seqfveqg  10935  seq3fveq  10936  ser3mono  10944  seqsplitg  10946  seqcaopr2g  10951  iseqf1olemkle  10954  seq3f1olemqsumkj  10968  seq3f1olemqsumk  10969  seqf1oglem2  10977  seqf1og  10978  seq3id  10982  seq3z  10985  seqhomog  10987  le2sq2  11072  bcpasc  11225  fihasheqf1oi  11247  seq3coll  11315  wrdnval  11356  wrdsymb1  11362  lswcl  11376  ccatlid  11395  ccatass  11397  ccat1st1st  11430  lswccats1fst  11433  swrdlsw  11462  ccatswrd  11463  pfxtrcfvl  11490  pfxsuff1eqwrdeq  11492  ccatpfx  11494  pfx1  11496  pfxswrd  11499  pfxlswccat  11506  swrdccatin2  11522  pfxccatin12  11526  caucvgrelemcau  11767  caucvgre  11768  r19.2uz  11780  sqrtgt0  11821  xrmaxiflemval  12040  clim2ser  12127  clim2ser2  12128  climub  12134  serf0  12142  fsumf1o  12181  fisumss  12183  fsumcl2lem  12189  fsumsplit  12198  fsum2dlemstep  12225  fisumrev2  12237  fsumlessfi  12251  telfsumo  12257  fsumparts  12261  fsumiun  12268  binom1dif  12278  isumsplit  12282  isumrpcl  12285  isumlessdc  12287  explecnv  12296  cvgratnnlemmn  12316  cvgratz  12323  cvgratgt0  12324  mertenslemi1  12326  clim2prod  12330  clim2divap  12331  fprodseq  12374  fprodf1o  12379  prodssdc  12380  fprodssdc  12381  fprodsplitdc  12387  fprodeq0  12408  fprod2dlemstep  12413  ef0lem  12451  eftlub  12481  tanval3ap  12505  dvdssubr  12630  divalgmod  12718  bitsdc  12738  bitsp1  12742  divgcdnn  12776  algfx  12854  eucalgcvga  12860  lcmcllem  12869  lcmneg  12876  isprm6  12950  cncongrprm  12960  nn0sqdcq  13012  phimullem  13031  pcid  13131  pcgcd  13136  pcz  13139  4sqlem9  13193  4sqlem15  13212  4sqlem16  13213  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemsel1i  13313  ballotfilemsima  13316  ballotfilemfrceq  13329  imasex  13684  grpidd  13761  gzsumress  13770  ismndd  13808  subsubm  13848  grpinvid1  13915  grpinvid2  13916  grplcan  13925  grpinvinv  13930  grpinvval2  13946  mulgass  14020  mulgpropdg  14025  subginv  14042  subgmulg  14049  issubg2m  14050  issubg4m  14054  subsubg  14058  eqger  14085  qusinv  14097  resghm  14121  conjsubgen  14139  gsum2dfilem2  14271  rngrz  14351  isrngd  14358  ringidss  14440  isringd  14452  ringlz  14454  ringrz  14455  unitgrp  14531  0unit  14544  unitnegcl  14545  dvrass  14554  dvreq1  14557  dvrdir  14558  ringinvdv  14560  invrpropdg  14564  rhmunitinv  14593  issubrng2  14626  subsubrng  14630  subrg1  14647  issubrg2  14657  subsubrg  14661  lmod0vs  14766  lmodvs0  14767  lmodvneg1  14775  islss3  14824  lspsnsubg  14841  lspid  14842  lspssv  14843  lspidm  14846  lspsnneg  14865  sraval  14882  qus1  14971  zringmulg  15041  mulgrhm  15052  znidom  15100  issubassa3  15120  psrass1filem  15186  psrlidmfi  15208  tgcl  15307  tgclb  15308  tgss2  15322  ntrss3  15366  ntridm  15369  opnssneib  15399  ssnei2  15400  innei  15406  resttopon  15414  cnpnei  15462  cnntri  15467  lmss  15489  txcnp  15514  blpnfctr  15682  mopni2  15726  bdmopn  15747  climcncf  15827  ivthdec  15887  cnplimcim  15910  dvconst  15937  dvconstre  15939  dvef  15970  plymullem  15993  plycoeid3  16000  rpcxpneg  16157  abscxp  16167  log2tlbndlog2  16237  birthdaylem2  16243  ppiqsval  16257  ppiprm  16276  chtprm  16278  chtdif  16281  ppiqltx  16298  prmorcht  16299  sgmmul  16307  chtqleppi  16311  chtublem  16312  bposlem3  16330  lgscllem  16348  lgsvalmod  16360  lgsdir2  16374  lgsquadlem2  16419  lgsquad2lem2  16423  upgredg  16607  usgruspgrben  16649  usgredg3  16677  cvgcmp2nlemabs  17304  trilpolemisumle  17311  trilpolemeq1  17313  trilpolemlt1  17314  nconstwlpolemgt0  17338  neapmkvlem  17341