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  6624  tfrcllemres  6637  tfri3  6642  ixpexgg  7008  f1domg  7048  fundmfi  7255  f1ofi  7261  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  9750  qreccl  10058  xrrege0  10244  peano2fzor  10667  flqltnz  10743  flqdiv  10779  zmodcl  10802  frecuzrdgtcl  10870  frecuzrdgfunlem  10877  seqfveqg  10936  seq3fveq  10937  ser3mono  10945  seqsplitg  10947  seqcaopr2g  10952  iseqf1olemkle  10955  seq3f1olemqsumkj  10969  seq3f1olemqsumk  10970  seqf1oglem2  10978  seqf1og  10979  seq3id  10983  seq3z  10986  seqhomog  10988  le2sq2  11073  bcpasc  11226  fihasheqf1oi  11248  seq3coll  11316  wrdnval  11357  wrdsymb1  11363  lswcl  11377  ccatlid  11396  ccatass  11398  ccat1st1st  11431  lswccats1fst  11434  swrdlsw  11463  ccatswrd  11464  pfxtrcfvl  11491  pfxsuff1eqwrdeq  11493  ccatpfx  11495  pfx1  11497  pfxswrd  11500  pfxlswccat  11507  swrdccatin2  11523  pfxccatin12  11527  caucvgrelemcau  11768  caucvgre  11769  r19.2uz  11781  sqrtgt0  11822  xrmaxiflemval  12041  clim2ser  12128  clim2ser2  12129  climub  12135  serf0  12143  fsumf1o  12182  fisumss  12184  fsumcl2lem  12190  fsumsplit  12199  fsum2dlemstep  12226  fisumrev2  12238  fsumlessfi  12252  telfsumo  12258  fsumparts  12262  fsumiun  12269  binom1dif  12279  isumsplit  12283  isumrpcl  12286  isumlessdc  12288  explecnv  12297  cvgratnnlemmn  12317  cvgratz  12324  cvgratgt0  12325  mertenslemi1  12327  clim2prod  12331  clim2divap  12332  fprodseq  12375  fprodf1o  12380  prodssdc  12381  fprodssdc  12382  fprodsplitdc  12388  fprodeq0  12409  fprod2dlemstep  12414  ef0lem  12452  eftlub  12482  tanval3ap  12506  dvdssubr  12631  divalgmod  12719  bitsdc  12739  bitsp1  12743  divgcdnn  12777  algfx  12855  eucalgcvga  12861  lcmcllem  12870  lcmneg  12877  isprm6  12951  cncongrprm  12961  nn0sqdcq  13013  phimullem  13032  pcid  13132  pcgcd  13137  pcz  13140  4sqlem9  13194  4sqlem15  13213  4sqlem16  13214  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemsel1i  13314  ballotfilemsima  13317  ballotfilemfrceq  13330  imasex  13685  grpidd  13762  gzsumress  13771  ismndd  13809  subsubm  13849  grpinvid1  13916  grpinvid2  13917  grplcan  13926  grpinvinv  13931  grpinvval2  13947  mulgass  14021  mulgpropdg  14026  subginv  14043  subgmulg  14050  issubg2m  14051  issubg4m  14055  subsubg  14059  eqger  14086  qusinv  14098  resghm  14122  conjsubgen  14140  gsum2dfilem2  14272  rngrz  14352  isrngd  14359  ringidss  14441  isringd  14453  ringlz  14455  ringrz  14456  unitgrp  14532  0unit  14545  unitnegcl  14546  dvrass  14555  dvreq1  14558  dvrdir  14559  ringinvdv  14561  invrpropdg  14565  rhmunitinv  14594  issubrng2  14627  subsubrng  14631  subrg1  14648  issubrg2  14658  subsubrg  14662  lmod0vs  14767  lmodvs0  14768  lmodvneg1  14776  islss3  14825  lspsnsubg  14842  lspid  14843  lspssv  14844  lspidm  14847  lspsnneg  14866  sraval  14883  qus1  14972  zringmulg  15042  mulgrhm  15053  znidom  15101  issubassa3  15121  psrass1filem  15177  psrlidmfi  15199  tgcl  15290  tgclb  15291  tgss2  15305  ntrss3  15349  ntridm  15352  opnssneib  15382  ssnei2  15383  innei  15389  resttopon  15397  cnpnei  15445  cnntri  15450  lmss  15472  txcnp  15497  blpnfctr  15665  mopni2  15709  bdmopn  15730  climcncf  15810  ivthdec  15870  cnplimcim  15893  dvconst  15920  dvconstre  15922  dvef  15953  plymullem  15976  plycoeid3  15983  rpcxpneg  16140  abscxp  16150  log2tlbndlog2  16220  birthdaylem2  16226  ppiqsval  16240  ppiprm  16259  chtprm  16261  chtdif  16264  ppiqltx  16281  prmorcht  16282  sgmmul  16290  chtqleppi  16294  chtublem  16295  bposlem3  16313  lgscllem  16331  lgsvalmod  16343  lgsdir2  16357  lgsquadlem2  16402  lgsquad2lem2  16406  upgredg  16590  usgruspgrben  16632  usgredg3  16660  cvgcmp2nlemabs  17287  trilpolemisumle  17294  trilpolemeq1  17296  trilpolemlt1  17297  nconstwlpolemgt0  17321  neapmkvlem  17324