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  7560  archnqq  7784  nqpru  7919  ltaddpr  7964  1idsr  8135  addgt0sr  8142  suplocsrlempr  8174  gt0ap0  8954  ap0gt0  8968  mulgt1  9193  gt0div  9200  ge0div  9201  ltdiv2  9217  creur  9289  avgle1  9546  recnz  9739  qreccl  10042  xrrege0  10227  peano2fzor  10650  flqltnz  10722  flqdiv  10758  zmodcl  10781  frecuzrdgtcl  10849  frecuzrdgfunlem  10856  seqfveqg  10915  seq3fveq  10916  ser3mono  10924  seqsplitg  10926  seqcaopr2g  10931  iseqf1olemkle  10934  seq3f1olemqsumkj  10948  seq3f1olemqsumk  10949  seqf1oglem2  10957  seqf1og  10958  seq3id  10962  seq3z  10965  seqhomog  10967  le2sq2  11052  bcpasc  11204  fihasheqf1oi  11226  seq3coll  11294  wrdnval  11335  wrdsymb1  11341  lswcl  11355  ccatlid  11374  ccatass  11376  ccat1st1st  11409  lswccats1fst  11412  swrdlsw  11441  ccatswrd  11442  pfxtrcfvl  11469  pfxsuff1eqwrdeq  11471  ccatpfx  11473  pfx1  11475  pfxswrd  11478  pfxlswccat  11485  swrdccatin2  11501  pfxccatin12  11505  caucvgrelemcau  11746  caucvgre  11747  r19.2uz  11759  sqrtgt0  11800  xrmaxiflemval  12016  clim2ser  12103  clim2ser2  12104  climub  12110  serf0  12118  fsumf1o  12157  fisumss  12159  fsumcl2lem  12165  fsumsplit  12174  fsum2dlemstep  12201  fisumrev2  12213  fsumlessfi  12227  telfsumo  12233  fsumparts  12237  fsumiun  12244  binom1dif  12254  isumsplit  12258  isumrpcl  12261  isumlessdc  12263  explecnv  12272  cvgratnnlemmn  12292  cvgratz  12299  cvgratgt0  12300  mertenslemi1  12302  clim2prod  12306  clim2divap  12307  fprodseq  12350  fprodf1o  12355  prodssdc  12356  fprodssdc  12357  fprodsplitdc  12363  fprodeq0  12384  fprod2dlemstep  12389  ef0lem  12427  eftlub  12457  tanval3ap  12481  dvdssubr  12606  divalgmod  12694  bitsdc  12714  bitsp1  12718  divgcdnn  12752  algfx  12830  eucalgcvga  12836  lcmcllem  12845  lcmneg  12852  isprm6  12925  cncongrprm  12935  phimullem  13003  pcid  13103  pcgcd  13108  pcz  13111  4sqlem9  13165  4sqlem15  13184  4sqlem16  13185  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemsel1i  13256  ballotfilemsima  13259  ballotfilemfrceq  13272  imasex  13626  grpidd  13703  gzsumress  13712  ismndd  13750  subsubm  13790  grpinvid1  13857  grpinvid2  13858  grplcan  13867  grpinvinv  13872  grpinvval2  13888  mulgass  13962  mulgpropdg  13967  subginv  13984  subgmulg  13991  issubg2m  13992  issubg4m  13996  subsubg  14000  eqger  14027  qusinv  14039  resghm  14063  conjsubgen  14081  rngrz  14245  isrngd  14252  ringidss  14334  isringd  14346  ringlz  14348  ringrz  14349  unitgrp  14423  0unit  14436  unitnegcl  14437  dvrass  14446  dvreq1  14449  dvrdir  14450  ringinvdv  14452  invrpropdg  14456  rhmunitinv  14485  issubrng2  14518  subsubrng  14522  subrg1  14539  issubrg2  14549  subsubrg  14553  lmod0vs  14658  lmodvs0  14659  lmodvneg1  14667  islss3  14716  lspsnsubg  14733  lspid  14734  lspssv  14735  lspidm  14738  lspsnneg  14757  sraval  14774  qus1  14863  zringmulg  14933  mulgrhm  14944  znidom  14992  issubassa3  15012  tgcl  15165  tgclb  15166  tgss2  15180  ntrss3  15224  ntridm  15227  opnssneib  15257  ssnei2  15258  innei  15264  resttopon  15272  cnpnei  15320  cnntri  15325  lmss  15347  txcnp  15372  blpnfctr  15540  mopni2  15584  bdmopn  15605  climcncf  15685  ivthdec  15745  cnplimcim  15768  dvconst  15795  dvconstre  15797  dvef  15828  plymullem  15851  plycoeid3  15858  rpcxpneg  16009  abscxp  16017  log2tlbndlog2  16082  birthdaylem2  16088  sgmmul  16110  lgscllem  16126  lgsvalmod  16138  lgsdir2  16152  lgsquadlem2  16197  lgsquad2lem2  16201  upgredg  16385  usgruspgrben  16427  usgredg3  16455  cvgcmp2nlemabs  17081  trilpolemisumle  17087  trilpolemeq1  17089  trilpolemlt1  17090  nconstwlpolemgt0  17114  neapmkvlem  17117