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  4292  pofun  4457  tfi  4729  fnbr  5485  caovlem2d  6282  caofcom  6333  fnexALT  6340  elabreximd  6356  tfr1onlemres  6620  tfrcllemres  6633  tfri3  6638  ixpexgg  7004  f1domg  7044  fundmfi  7251  f1ofi  7257  finacn  7561  archnqq  7785  nqpru  7920  ltaddpr  7965  1idsr  8136  addgt0sr  8143  suplocsrlempr  8175  gt0ap0  8957  ap0gt0  8971  mulgt1  9196  gt0div  9203  ge0div  9204  ltdiv2  9220  creur  9292  avgle1  9551  recnz  9744  qreccl  10052  xrrege0  10238  peano2fzor  10661  flqltnz  10737  flqdiv  10773  zmodcl  10796  frecuzrdgtcl  10864  frecuzrdgfunlem  10871  seqfveqg  10930  seq3fveq  10931  ser3mono  10939  seqsplitg  10941  seqcaopr2g  10946  iseqf1olemkle  10949  seq3f1olemqsumkj  10963  seq3f1olemqsumk  10964  seqf1oglem2  10972  seqf1og  10973  seq3id  10977  seq3z  10980  seqhomog  10982  le2sq2  11067  bcpasc  11220  fihasheqf1oi  11242  seq3coll  11310  wrdnval  11351  wrdsymb1  11357  lswcl  11371  ccatlid  11390  ccatass  11392  ccat1st1st  11425  lswccats1fst  11428  swrdlsw  11457  ccatswrd  11458  pfxtrcfvl  11485  pfxsuff1eqwrdeq  11487  ccatpfx  11489  pfx1  11491  pfxswrd  11494  pfxlswccat  11501  swrdccatin2  11517  pfxccatin12  11521  caucvgrelemcau  11762  caucvgre  11763  r19.2uz  11775  sqrtgt0  11816  xrmaxiflemval  12035  clim2ser  12122  clim2ser2  12123  climub  12129  serf0  12137  fsumf1o  12176  fisumss  12178  fsumcl2lem  12184  fsumsplit  12193  fsum2dlemstep  12220  fisumrev2  12232  fsumlessfi  12246  telfsumo  12252  fsumparts  12256  fsumiun  12263  binom1dif  12273  isumsplit  12277  isumrpcl  12280  isumlessdc  12282  explecnv  12291  cvgratnnlemmn  12311  cvgratz  12318  cvgratgt0  12319  mertenslemi1  12321  clim2prod  12325  clim2divap  12326  fprodseq  12369  fprodf1o  12374  prodssdc  12375  fprodssdc  12376  fprodsplitdc  12382  fprodeq0  12403  fprod2dlemstep  12408  ef0lem  12446  eftlub  12476  tanval3ap  12500  dvdssubr  12625  divalgmod  12713  bitsdc  12733  bitsp1  12737  divgcdnn  12771  algfx  12849  eucalgcvga  12855  lcmcllem  12864  lcmneg  12871  isprm6  12945  cncongrprm  12955  nn0sqdcq  13007  phimullem  13026  pcid  13126  pcgcd  13131  pcz  13134  4sqlem9  13188  4sqlem15  13207  4sqlem16  13208  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemsel1i  13308  ballotfilemsima  13311  ballotfilemfrceq  13324  imasex  13679  grpidd  13756  gzsumress  13765  ismndd  13803  subsubm  13843  grpinvid1  13910  grpinvid2  13911  grplcan  13920  grpinvinv  13925  grpinvval2  13941  mulgass  14015  mulgpropdg  14020  subginv  14037  subgmulg  14044  issubg2m  14045  issubg4m  14049  subsubg  14053  eqger  14080  qusinv  14092  resghm  14116  conjsubgen  14134  rngrz  14329  isrngd  14336  ringidss  14418  isringd  14430  ringlz  14432  ringrz  14433  unitgrp  14507  0unit  14520  unitnegcl  14521  dvrass  14530  dvreq1  14533  dvrdir  14534  ringinvdv  14536  invrpropdg  14540  rhmunitinv  14569  issubrng2  14602  subsubrng  14606  subrg1  14623  issubrg2  14633  subsubrg  14637  lmod0vs  14742  lmodvs0  14743  lmodvneg1  14751  islss3  14800  lspsnsubg  14817  lspid  14818  lspssv  14819  lspidm  14822  lspsnneg  14841  sraval  14858  qus1  14947  zringmulg  15017  mulgrhm  15028  znidom  15076  issubassa3  15096  tgcl  15256  tgclb  15257  tgss2  15271  ntrss3  15315  ntridm  15318  opnssneib  15348  ssnei2  15349  innei  15355  resttopon  15363  cnpnei  15411  cnntri  15416  lmss  15438  txcnp  15463  blpnfctr  15631  mopni2  15675  bdmopn  15696  climcncf  15776  ivthdec  15836  cnplimcim  15859  dvconst  15886  dvconstre  15888  dvef  15919  plymullem  15942  plycoeid3  15949  rpcxpneg  16104  abscxp  16112  log2tlbndlog2  16181  birthdaylem2  16187  ppiqsval  16201  ppiprm  16220  chtprm  16222  chtdif  16225  ppiqltx  16242  prmorcht  16243  sgmmul  16251  chtqleppi  16255  chtublem  16256  bposlem3  16274  lgscllem  16292  lgsvalmod  16304  lgsdir2  16318  lgsquadlem2  16363  lgsquad2lem2  16367  upgredg  16551  usgruspgrben  16593  usgredg3  16621  cvgcmp2nlemabs  17247  trilpolemisumle  17254  trilpolemeq1  17256  trilpolemlt1  17257  nconstwlpolemgt0  17281  neapmkvlem  17284