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  969  stoic2a  1474  sbcied2  3080  csbied2  3186  elpw2g  4268  pofun  4433  tfi  4704  fnbr  5460  caovlem2d  6247  caofcom  6297  fnexALT  6304  tfr1onlemres  6580  tfrcllemres  6593  tfri3  6598  ixpexgg  6957  f1domg  6997  fundmfi  7204  f1ofi  7210  finacn  7511  archnqq  7732  nqpru  7867  ltaddpr  7912  1idsr  8083  addgt0sr  8090  suplocsrlempr  8122  gt0ap0  8900  ap0gt0  8914  mulgt1  9137  gt0div  9144  ge0div  9145  ltdiv2  9161  creur  9233  avgle1  9479  recnz  9671  qreccl  9974  xrrege0  10158  peano2fzor  10577  flqltnz  10647  flqdiv  10683  zmodcl  10706  frecuzrdgtcl  10774  frecuzrdgfunlem  10781  seqfveqg  10840  seq3fveq  10841  ser3mono  10849  seqsplitg  10851  seqcaopr2g  10856  iseqf1olemkle  10859  seq3f1olemqsumkj  10873  seq3f1olemqsumk  10874  seqf1oglem2  10882  seqf1og  10883  seq3id  10887  seq3z  10890  seqhomog  10892  le2sq2  10977  bcpasc  11128  fihasheqf1oi  11150  seq3coll  11214  wrdnval  11255  wrdsymb1  11261  lswcl  11275  ccatlid  11294  ccatass  11296  ccat1st1st  11329  lswccats1fst  11332  swrdlsw  11361  ccatswrd  11362  pfxtrcfvl  11389  pfxsuff1eqwrdeq  11391  ccatpfx  11393  pfx1  11395  pfxswrd  11398  pfxlswccat  11405  swrdccatin2  11421  pfxccatin12  11425  caucvgrelemcau  11665  caucvgre  11666  r19.2uz  11678  sqrtgt0  11719  xrmaxiflemval  11935  clim2ser  12022  clim2ser2  12023  climub  12029  serf0  12037  fsumf1o  12076  fisumss  12078  fsumcl2lem  12084  fsumsplit  12093  fsum2dlemstep  12120  fisumrev2  12132  fsumlessfi  12146  telfsumo  12152  fsumparts  12156  fsumiun  12163  binom1dif  12173  isumsplit  12177  isumrpcl  12180  isumlessdc  12182  explecnv  12191  cvgratnnlemmn  12211  cvgratz  12218  cvgratgt0  12219  mertenslemi1  12221  clim2prod  12225  clim2divap  12226  fprodseq  12269  fprodf1o  12274  prodssdc  12275  fprodssdc  12276  fprodsplitdc  12282  fprodeq0  12303  fprod2dlemstep  12308  ef0lem  12346  eftlub  12376  tanval3ap  12400  dvdssubr  12525  divalgmod  12613  bitsdc  12633  bitsp1  12637  divgcdnn  12671  algfx  12749  eucalgcvga  12755  lcmcllem  12764  lcmneg  12771  isprm6  12844  cncongrprm  12854  phimullem  12922  pcid  13022  pcgcd  13027  pcz  13030  4sqlem9  13084  4sqlem15  13103  4sqlem16  13104  imasex  13518  grpidd  13596  gsumress  13608  ismndd  13650  subsubm  13696  grpinvid1  13765  grpinvid2  13766  grplcan  13775  grpinvinv  13780  grpinvval2  13796  mulgass  13876  mulgpropdg  13881  subginv  13898  subgmulg  13905  issubg2m  13906  issubg4m  13910  subsubg  13914  eqger  13941  qusinv  13953  resghm  13977  conjsubgen  13995  rngrz  14090  isrngd  14097  ringidss  14173  isringd  14185  ringlz  14187  ringrz  14188  unitgrp  14261  0unit  14274  unitnegcl  14275  dvrass  14284  dvreq1  14287  dvrdir  14288  ringinvdv  14290  invrpropdg  14294  rhmunitinv  14323  issubrng2  14355  subsubrng  14359  subrg1  14376  issubrg2  14386  subsubrg  14390  lmod0vs  14469  lmodvs0  14470  lmodvneg1  14478  islss3  14527  lspsnsubg  14544  lspid  14545  lspssv  14546  lspidm  14549  lspsnneg  14568  sraval  14585  qus1  14674  zringmulg  14746  mulgrhm  14757  znidom  14805  tgcl  14929  tgclb  14930  tgss2  14944  ntrss3  14988  ntridm  14991  opnssneib  15021  ssnei2  15022  innei  15028  resttopon  15036  cnpnei  15084  cnntri  15089  lmss  15111  txcnp  15136  blpnfctr  15304  mopni2  15348  bdmopn  15369  climcncf  15449  ivthdec  15509  cnplimcim  15532  dvconst  15559  dvconstre  15561  dvef  15592  plymullem  15615  plycoeid3  15622  rpcxpneg  15772  abscxp  15780  sgmmul  15864  lgscllem  15880  lgsvalmod  15892  lgsdir2  15906  lgsquadlem2  15951  lgsquad2lem2  15955  upgredg  16139  usgruspgrben  16181  usgredg3  16209  cvgcmp2nlemabs  16816  trilpolemisumle  16822  trilpolemeq1  16824  trilpolemlt1  16825  nconstwlpolemgt0  16850  neapmkvlem  16853