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  968  stoic2a  1473  sbcied2  3069  csbied2  3175  elpw2g  4246  pofun  4409  tfi  4680  fnbr  5434  caovlem2d  6215  caofcom  6266  fnexALT  6273  tfr1onlemres  6515  tfrcllemres  6528  tfri3  6533  ixpexgg  6891  f1domg  6931  fundmfi  7136  f1ofi  7142  finacn  7419  archnqq  7637  nqpru  7772  ltaddpr  7817  1idsr  7988  addgt0sr  7995  suplocsrlempr  8027  gt0ap0  8806  ap0gt0  8820  mulgt1  9043  gt0div  9050  ge0div  9051  ltdiv2  9067  creur  9139  avgle1  9385  recnz  9573  qreccl  9876  xrrege0  10060  peano2fzor  10478  flqltnz  10548  flqdiv  10584  zmodcl  10607  frecuzrdgtcl  10675  frecuzrdgfunlem  10682  seqfveqg  10741  seq3fveq  10742  ser3mono  10750  seqsplitg  10752  seqcaopr2g  10757  iseqf1olemkle  10760  seq3f1olemqsumkj  10774  seq3f1olemqsumk  10775  seqf1oglem2  10783  seqf1og  10784  seq3id  10788  seq3z  10791  seqhomog  10793  le2sq2  10878  bcpasc  11029  fihasheqf1oi  11050  seq3coll  11107  wrdnval  11148  wrdsymb1  11154  lswcl  11168  ccatlid  11187  ccatass  11189  ccat1st1st  11222  lswccats1fst  11225  swrdlsw  11254  ccatswrd  11255  pfxtrcfvl  11282  pfxsuff1eqwrdeq  11284  ccatpfx  11286  pfx1  11288  pfxswrd  11291  pfxlswccat  11298  swrdccatin2  11314  pfxccatin12  11318  caucvgrelemcau  11558  caucvgre  11559  r19.2uz  11571  sqrtgt0  11612  xrmaxiflemval  11828  clim2ser  11915  clim2ser2  11916  climub  11922  serf0  11930  fsumf1o  11969  fisumss  11971  fsumcl2lem  11977  fsumsplit  11986  fsum2dlemstep  12013  fisumrev2  12025  fsumlessfi  12039  telfsumo  12045  fsumparts  12049  fsumiun  12056  binom1dif  12066  isumsplit  12070  isumrpcl  12073  isumlessdc  12075  explecnv  12084  cvgratnnlemmn  12104  cvgratz  12111  cvgratgt0  12112  mertenslemi1  12114  clim2prod  12118  clim2divap  12119  fprodseq  12162  fprodf1o  12167  prodssdc  12168  fprodssdc  12169  fprodsplitdc  12175  fprodeq0  12196  fprod2dlemstep  12201  ef0lem  12239  eftlub  12269  tanval3ap  12293  dvdssubr  12418  divalgmod  12506  bitsdc  12526  bitsp1  12530  divgcdnn  12564  algfx  12642  eucalgcvga  12648  lcmcllem  12657  lcmneg  12664  isprm6  12737  cncongrprm  12747  phimullem  12815  pcid  12915  pcgcd  12920  pcz  12923  4sqlem9  12977  4sqlem15  12996  4sqlem16  12997  imasex  13406  grpidd  13484  gsumress  13496  ismndd  13538  subsubm  13584  grpinvid1  13653  grpinvid2  13654  grplcan  13663  grpinvinv  13668  grpinvval2  13684  mulgass  13764  mulgpropdg  13769  subginv  13786  subgmulg  13793  issubg2m  13794  issubg4m  13798  subsubg  13802  eqger  13829  qusinv  13841  resghm  13865  conjsubgen  13883  rngrz  13978  isrngd  13985  ringidss  14061  isringd  14073  ringlz  14075  ringrz  14076  unitgrp  14149  0unit  14162  unitnegcl  14163  dvrass  14172  dvreq1  14175  dvrdir  14176  ringinvdv  14178  invrpropdg  14182  rhmunitinv  14211  issubrng2  14243  subsubrng  14247  subrg1  14264  issubrg2  14274  subsubrg  14278  lmod0vs  14354  lmodvs0  14355  lmodvneg1  14363  islss3  14412  lspsnsubg  14429  lspid  14430  lspssv  14431  lspidm  14434  lspsnneg  14453  sraval  14470  qus1  14559  zringmulg  14631  mulgrhm  14642  znidom  14690  tgcl  14807  tgclb  14808  tgss2  14822  ntrss3  14866  ntridm  14869  opnssneib  14899  ssnei2  14900  innei  14906  resttopon  14914  cnpnei  14962  cnntri  14967  lmss  14989  txcnp  15014  blpnfctr  15182  mopni2  15226  bdmopn  15247  climcncf  15327  ivthdec  15387  cnplimcim  15410  dvconst  15437  dvconstre  15439  dvef  15470  plymullem  15493  plycoeid3  15500  rpcxpneg  15650  abscxp  15658  sgmmul  15739  lgscllem  15755  lgsvalmod  15767  lgsdir2  15781  lgsquadlem2  15826  lgsquad2lem2  15830  upgredg  16014  usgruspgrben  16056  usgredg3  16084  cvgcmp2nlemabs  16687  trilpolemisumle  16693  trilpolemeq1  16695  trilpolemlt1  16696  nconstwlpolemgt0  16720  neapmkvlem  16723