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  963  stoic2a  1449  sbcied2  3036  csbied2  3141  elpw2g  4201  pofun  4360  tfi  4631  fnbr  5379  caovlem2d  6141  caofcom  6191  fnexALT  6198  tfr1onlemres  6437  tfrcllemres  6450  tfri3  6455  ixpexgg  6811  f1domg  6851  fundmfi  7041  f1ofi  7047  finacn  7318  archnqq  7532  nqpru  7667  ltaddpr  7712  1idsr  7883  addgt0sr  7890  suplocsrlempr  7922  gt0ap0  8701  ap0gt0  8715  mulgt1  8938  gt0div  8945  ge0div  8946  ltdiv2  8962  creur  9034  avgle1  9280  recnz  9468  qreccl  9765  xrrege0  9949  peano2fzor  10363  flqltnz  10432  flqdiv  10468  zmodcl  10491  frecuzrdgtcl  10559  frecuzrdgfunlem  10566  seqfveqg  10625  seq3fveq  10626  ser3mono  10634  seqsplitg  10636  seqcaopr2g  10641  iseqf1olemkle  10644  seq3f1olemqsumkj  10658  seq3f1olemqsumk  10659  seqf1oglem2  10667  seqf1og  10668  seq3id  10672  seq3z  10675  seqhomog  10677  le2sq2  10762  bcpasc  10913  fihasheqf1oi  10934  seq3coll  10989  wrdnval  11026  wrdsymb1  11032  lswcl  11046  ccatlid  11065  ccatass  11067  ccat1st1st  11096  lswccats1fst  11099  swrdlsw  11125  ccatswrd  11126  pfxtrcfvl  11151  pfxsuff1eqwrdeq  11153  ccatpfx  11155  pfx1  11157  caucvgrelemcau  11324  caucvgre  11325  r19.2uz  11337  sqrtgt0  11378  xrmaxiflemval  11594  clim2ser  11681  clim2ser2  11682  climub  11688  serf0  11696  fsumf1o  11734  fisumss  11736  fsumcl2lem  11742  fsumsplit  11751  fsum2dlemstep  11778  fisumrev2  11790  fsumlessfi  11804  telfsumo  11810  fsumparts  11814  fsumiun  11821  binom1dif  11831  isumsplit  11835  isumrpcl  11838  isumlessdc  11840  explecnv  11849  cvgratnnlemmn  11869  cvgratz  11876  cvgratgt0  11877  mertenslemi1  11879  clim2prod  11883  clim2divap  11884  fprodseq  11927  fprodf1o  11932  prodssdc  11933  fprodssdc  11934  fprodsplitdc  11940  fprodeq0  11961  fprod2dlemstep  11966  ef0lem  12004  eftlub  12034  tanval3ap  12058  dvdssubr  12183  divalgmod  12271  bitsdc  12291  bitsp1  12295  divgcdnn  12329  algfx  12407  eucalgcvga  12413  lcmcllem  12422  lcmneg  12429  isprm6  12502  cncongrprm  12512  phimullem  12580  pcid  12680  pcgcd  12685  pcz  12688  4sqlem9  12742  4sqlem15  12761  4sqlem16  12762  imasex  13170  grpidd  13248  gsumress  13260  ismndd  13302  subsubm  13348  grpinvid1  13417  grpinvid2  13418  grplcan  13427  grpinvinv  13432  grpinvval2  13448  mulgass  13528  mulgpropdg  13533  subginv  13550  subgmulg  13557  issubg2m  13558  issubg4m  13562  subsubg  13566  eqger  13593  qusinv  13605  resghm  13629  conjsubgen  13647  rngrz  13741  isrngd  13748  ringidss  13824  isringd  13836  ringlz  13838  ringrz  13839  unitgrp  13911  0unit  13924  unitnegcl  13925  dvrass  13934  dvreq1  13937  dvrdir  13938  ringinvdv  13940  invrpropdg  13944  rhmunitinv  13973  issubrng2  14005  subsubrng  14009  subrg1  14026  issubrg2  14036  subsubrg  14040  lmod0vs  14116  lmodvs0  14117  lmodvneg1  14125  islss3  14174  lspsnsubg  14191  lspid  14192  lspssv  14193  lspidm  14196  lspsnneg  14215  sraval  14232  qus1  14321  zringmulg  14393  mulgrhm  14404  znidom  14452  tgcl  14569  tgclb  14570  tgss2  14584  ntrss3  14628  ntridm  14631  opnssneib  14661  ssnei2  14662  innei  14668  resttopon  14676  cnpnei  14724  cnntri  14729  lmss  14751  txcnp  14776  blpnfctr  14944  mopni2  14988  bdmopn  15009  climcncf  15089  ivthdec  15149  cnplimcim  15172  dvconst  15199  dvconstre  15201  dvef  15232  plymullem  15255  plycoeid3  15262  rpcxpneg  15412  abscxp  15420  sgmmul  15501  lgscllem  15517  lgsvalmod  15529  lgsdir2  15543  lgsquadlem2  15588  lgsquad2lem2  15592  cvgcmp2nlemabs  16008  trilpolemisumle  16014  trilpolemeq1  16016  trilpolemlt1  16017  nconstwlpolemgt0  16040  neapmkvlem  16043