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  6214  caofcom  6265  fnexALT  6272  tfr1onlemres  6514  tfrcllemres  6527  tfri3  6532  ixpexgg  6890  f1domg  6930  fundmfi  7135  f1ofi  7141  finacn  7418  archnqq  7636  nqpru  7771  ltaddpr  7816  1idsr  7987  addgt0sr  7994  suplocsrlempr  8026  gt0ap0  8805  ap0gt0  8819  mulgt1  9042  gt0div  9049  ge0div  9050  ltdiv2  9066  creur  9138  avgle1  9384  recnz  9572  qreccl  9875  xrrege0  10059  peano2fzor  10476  flqltnz  10546  flqdiv  10582  zmodcl  10605  frecuzrdgtcl  10673  frecuzrdgfunlem  10680  seqfveqg  10739  seq3fveq  10740  ser3mono  10748  seqsplitg  10750  seqcaopr2g  10755  iseqf1olemkle  10758  seq3f1olemqsumkj  10772  seq3f1olemqsumk  10773  seqf1oglem2  10781  seqf1og  10782  seq3id  10786  seq3z  10789  seqhomog  10791  le2sq2  10876  bcpasc  11027  fihasheqf1oi  11048  seq3coll  11105  wrdnval  11143  wrdsymb1  11149  lswcl  11163  ccatlid  11182  ccatass  11184  ccat1st1st  11217  lswccats1fst  11220  swrdlsw  11249  ccatswrd  11250  pfxtrcfvl  11277  pfxsuff1eqwrdeq  11279  ccatpfx  11281  pfx1  11283  pfxswrd  11286  pfxlswccat  11293  swrdccatin2  11309  pfxccatin12  11313  caucvgrelemcau  11540  caucvgre  11541  r19.2uz  11553  sqrtgt0  11594  xrmaxiflemval  11810  clim2ser  11897  clim2ser2  11898  climub  11904  serf0  11912  fsumf1o  11950  fisumss  11952  fsumcl2lem  11958  fsumsplit  11967  fsum2dlemstep  11994  fisumrev2  12006  fsumlessfi  12020  telfsumo  12026  fsumparts  12030  fsumiun  12037  binom1dif  12047  isumsplit  12051  isumrpcl  12054  isumlessdc  12056  explecnv  12065  cvgratnnlemmn  12085  cvgratz  12092  cvgratgt0  12093  mertenslemi1  12095  clim2prod  12099  clim2divap  12100  fprodseq  12143  fprodf1o  12148  prodssdc  12149  fprodssdc  12150  fprodsplitdc  12156  fprodeq0  12177  fprod2dlemstep  12182  ef0lem  12220  eftlub  12250  tanval3ap  12274  dvdssubr  12399  divalgmod  12487  bitsdc  12507  bitsp1  12511  divgcdnn  12545  algfx  12623  eucalgcvga  12629  lcmcllem  12638  lcmneg  12645  isprm6  12718  cncongrprm  12728  phimullem  12796  pcid  12896  pcgcd  12901  pcz  12904  4sqlem9  12958  4sqlem15  12977  4sqlem16  12978  imasex  13387  grpidd  13465  gsumress  13477  ismndd  13519  subsubm  13565  grpinvid1  13634  grpinvid2  13635  grplcan  13644  grpinvinv  13649  grpinvval2  13665  mulgass  13745  mulgpropdg  13750  subginv  13767  subgmulg  13774  issubg2m  13775  issubg4m  13779  subsubg  13783  eqger  13810  qusinv  13822  resghm  13846  conjsubgen  13864  rngrz  13958  isrngd  13965  ringidss  14041  isringd  14053  ringlz  14055  ringrz  14056  unitgrp  14129  0unit  14142  unitnegcl  14143  dvrass  14152  dvreq1  14155  dvrdir  14156  ringinvdv  14158  invrpropdg  14162  rhmunitinv  14191  issubrng2  14223  subsubrng  14227  subrg1  14244  issubrg2  14254  subsubrg  14258  lmod0vs  14334  lmodvs0  14335  lmodvneg1  14343  islss3  14392  lspsnsubg  14409  lspid  14410  lspssv  14411  lspidm  14414  lspsnneg  14433  sraval  14450  qus1  14539  zringmulg  14611  mulgrhm  14622  znidom  14670  tgcl  14787  tgclb  14788  tgss2  14802  ntrss3  14846  ntridm  14849  opnssneib  14879  ssnei2  14880  innei  14886  resttopon  14894  cnpnei  14942  cnntri  14947  lmss  14969  txcnp  14994  blpnfctr  15162  mopni2  15206  bdmopn  15227  climcncf  15307  ivthdec  15367  cnplimcim  15390  dvconst  15417  dvconstre  15419  dvef  15450  plymullem  15473  plycoeid3  15480  rpcxpneg  15630  abscxp  15638  sgmmul  15719  lgscllem  15735  lgsvalmod  15747  lgsdir2  15761  lgsquadlem2  15806  lgsquad2lem2  15810  upgredg  15994  usgruspgrben  16036  usgredg3  16064  cvgcmp2nlemabs  16636  trilpolemisumle  16642  trilpolemeq1  16644  trilpolemlt1  16645  nconstwlpolemgt0  16668  neapmkvlem  16671