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  3070  csbied2  3176  elpw2g  4251  pofun  4415  tfi  4686  fnbr  5441  caovlem2d  6225  caofcom  6275  fnexALT  6282  tfr1onlemres  6558  tfrcllemres  6571  tfri3  6576  ixpexgg  6934  f1domg  6974  fundmfi  7179  f1ofi  7185  finacn  7479  archnqq  7697  nqpru  7832  ltaddpr  7877  1idsr  8048  addgt0sr  8055  suplocsrlempr  8087  gt0ap0  8865  ap0gt0  8879  mulgt1  9102  gt0div  9109  ge0div  9110  ltdiv2  9126  creur  9198  avgle1  9444  recnz  9634  qreccl  9937  xrrege0  10121  peano2fzor  10540  flqltnz  10610  flqdiv  10646  zmodcl  10669  frecuzrdgtcl  10737  frecuzrdgfunlem  10744  seqfveqg  10803  seq3fveq  10804  ser3mono  10812  seqsplitg  10814  seqcaopr2g  10819  iseqf1olemkle  10822  seq3f1olemqsumkj  10836  seq3f1olemqsumk  10837  seqf1oglem2  10845  seqf1og  10846  seq3id  10850  seq3z  10853  seqhomog  10855  le2sq2  10940  bcpasc  11091  fihasheqf1oi  11112  seq3coll  11169  wrdnval  11210  wrdsymb1  11216  lswcl  11230  ccatlid  11249  ccatass  11251  ccat1st1st  11284  lswccats1fst  11287  swrdlsw  11316  ccatswrd  11317  pfxtrcfvl  11344  pfxsuff1eqwrdeq  11346  ccatpfx  11348  pfx1  11350  pfxswrd  11353  pfxlswccat  11360  swrdccatin2  11376  pfxccatin12  11380  caucvgrelemcau  11620  caucvgre  11621  r19.2uz  11633  sqrtgt0  11674  xrmaxiflemval  11890  clim2ser  11977  clim2ser2  11978  climub  11984  serf0  11992  fsumf1o  12031  fisumss  12033  fsumcl2lem  12039  fsumsplit  12048  fsum2dlemstep  12075  fisumrev2  12087  fsumlessfi  12101  telfsumo  12107  fsumparts  12111  fsumiun  12118  binom1dif  12128  isumsplit  12132  isumrpcl  12135  isumlessdc  12137  explecnv  12146  cvgratnnlemmn  12166  cvgratz  12173  cvgratgt0  12174  mertenslemi1  12176  clim2prod  12180  clim2divap  12181  fprodseq  12224  fprodf1o  12229  prodssdc  12230  fprodssdc  12231  fprodsplitdc  12237  fprodeq0  12258  fprod2dlemstep  12263  ef0lem  12301  eftlub  12331  tanval3ap  12355  dvdssubr  12480  divalgmod  12568  bitsdc  12588  bitsp1  12592  divgcdnn  12626  algfx  12704  eucalgcvga  12710  lcmcllem  12719  lcmneg  12726  isprm6  12799  cncongrprm  12809  phimullem  12877  pcid  12977  pcgcd  12982  pcz  12985  4sqlem9  13039  4sqlem15  13058  4sqlem16  13059  imasex  13468  grpidd  13546  gsumress  13558  ismndd  13600  subsubm  13646  grpinvid1  13715  grpinvid2  13716  grplcan  13725  grpinvinv  13730  grpinvval2  13746  mulgass  13826  mulgpropdg  13831  subginv  13848  subgmulg  13855  issubg2m  13856  issubg4m  13860  subsubg  13864  eqger  13891  qusinv  13903  resghm  13927  conjsubgen  13945  rngrz  14040  isrngd  14047  ringidss  14123  isringd  14135  ringlz  14137  ringrz  14138  unitgrp  14211  0unit  14224  unitnegcl  14225  dvrass  14234  dvreq1  14237  dvrdir  14238  ringinvdv  14240  invrpropdg  14244  rhmunitinv  14273  issubrng2  14305  subsubrng  14309  subrg1  14326  issubrg2  14336  subsubrg  14340  lmod0vs  14417  lmodvs0  14418  lmodvneg1  14426  islss3  14475  lspsnsubg  14492  lspid  14493  lspssv  14494  lspidm  14497  lspsnneg  14516  sraval  14533  qus1  14622  zringmulg  14694  mulgrhm  14705  znidom  14753  tgcl  14875  tgclb  14876  tgss2  14890  ntrss3  14934  ntridm  14937  opnssneib  14967  ssnei2  14968  innei  14974  resttopon  14982  cnpnei  15030  cnntri  15035  lmss  15057  txcnp  15082  blpnfctr  15250  mopni2  15294  bdmopn  15315  climcncf  15395  ivthdec  15455  cnplimcim  15478  dvconst  15505  dvconstre  15507  dvef  15538  plymullem  15561  plycoeid3  15568  rpcxpneg  15718  abscxp  15726  sgmmul  15810  lgscllem  15826  lgsvalmod  15838  lgsdir2  15852  lgsquadlem2  15897  lgsquad2lem2  15901  upgredg  16085  usgruspgrben  16127  usgredg3  16155  cvgcmp2nlemabs  16764  trilpolemisumle  16770  trilpolemeq1  16772  trilpolemlt1  16773  nconstwlpolemgt0  16797  neapmkvlem  16800