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  962  stoic2a  1440  sbcied2  3023  csbied2  3128  elpw2g  4185  pofun  4343  tfi  4614  fnbr  5356  caovlem2d  6111  caofcom  6156  fnexALT  6163  tfr1onlemres  6402  tfrcllemres  6415  tfri3  6420  ixpexgg  6776  f1domg  6812  fundmfi  6996  f1ofi  7002  archnqq  7477  nqpru  7612  ltaddpr  7657  1idsr  7828  addgt0sr  7835  suplocsrlempr  7867  gt0ap0  8645  ap0gt0  8659  mulgt1  8882  gt0div  8889  ge0div  8890  ltdiv2  8906  creur  8978  avgle1  9223  recnz  9410  qreccl  9707  xrrege0  9891  peano2fzor  10299  flqltnz  10356  flqdiv  10392  zmodcl  10415  frecuzrdgtcl  10483  frecuzrdgfunlem  10490  seqfveqg  10549  seq3fveq  10550  ser3mono  10558  seqsplitg  10560  seqcaopr2g  10565  iseqf1olemkle  10568  seq3f1olemqsumkj  10582  seq3f1olemqsumk  10583  seqf1oglem2  10591  seqf1og  10592  seq3id  10596  seq3z  10599  seqhomog  10601  le2sq2  10686  bcpasc  10837  fihasheqf1oi  10858  seq3coll  10913  wrdnval  10944  wrdsymb1  10950  caucvgrelemcau  11124  caucvgre  11125  r19.2uz  11137  sqrtgt0  11178  xrmaxiflemval  11393  clim2ser  11480  clim2ser2  11481  climub  11487  serf0  11495  fsumf1o  11533  fisumss  11535  fsumcl2lem  11541  fsumsplit  11550  fsum2dlemstep  11577  fisumrev2  11589  fsumlessfi  11603  telfsumo  11609  fsumparts  11613  fsumiun  11620  binom1dif  11630  isumsplit  11634  isumrpcl  11637  isumlessdc  11639  explecnv  11648  cvgratnnlemmn  11668  cvgratz  11675  cvgratgt0  11676  mertenslemi1  11678  clim2prod  11682  clim2divap  11683  fprodseq  11726  fprodf1o  11731  prodssdc  11732  fprodssdc  11733  fprodsplitdc  11739  fprodeq0  11760  fprod2dlemstep  11765  ef0lem  11803  eftlub  11833  tanval3ap  11857  dvdssubr  11982  divalgmod  12068  divgcdnn  12112  algfx  12190  eucalgcvga  12196  lcmcllem  12205  lcmneg  12212  isprm6  12285  cncongrprm  12295  phimullem  12363  pcid  12462  pcgcd  12467  pcz  12470  4sqlem9  12524  4sqlem15  12543  4sqlem16  12544  imasex  12888  grpidd  12966  gsumress  12978  ismndd  13018  subsubm  13055  grpinvid1  13124  grpinvid2  13125  grplcan  13134  grpinvinv  13139  grpinvval2  13155  mulgass  13229  mulgpropdg  13234  subginv  13251  subgmulg  13258  issubg2m  13259  issubg4m  13263  subsubg  13267  eqger  13294  qusinv  13306  resghm  13330  conjsubgen  13348  rngrz  13442  isrngd  13449  ringidss  13525  isringd  13537  ringlz  13539  ringrz  13540  unitgrp  13612  0unit  13625  unitnegcl  13626  dvrass  13635  dvreq1  13638  dvrdir  13639  ringinvdv  13641  invrpropdg  13645  rhmunitinv  13674  issubrng2  13706  subsubrng  13710  subrg1  13727  issubrg2  13737  subsubrg  13741  lmod0vs  13817  lmodvs0  13818  lmodvneg1  13826  islss3  13875  lspsnsubg  13892  lspid  13893  lspssv  13894  lspidm  13897  lspsnneg  13916  sraval  13933  qus1  14022  zringmulg  14086  mulgrhm  14097  znidom  14145  tgcl  14232  tgclb  14233  tgss2  14247  ntrss3  14291  ntridm  14294  opnssneib  14324  ssnei2  14325  innei  14331  resttopon  14339  cnpnei  14387  cnntri  14392  lmss  14414  txcnp  14439  blpnfctr  14607  mopni2  14651  bdmopn  14672  climcncf  14739  ivthdec  14798  cnplimcim  14821  dvconst  14846  dvef  14873  plymullem  14896  rpcxpneg  15042  abscxp  15049  lgscllem  15123  lgsvalmod  15135  lgsdir2  15149  cvgcmp2nlemabs  15522  trilpolemisumle  15528  trilpolemeq1  15530  trilpolemlt1  15531  nconstwlpolemgt0  15554  neapmkvlem  15557