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  966  stoic2a  1471  sbcied2  3066  csbied2  3172  elpw2g  4240  pofun  4403  tfi  4674  fnbr  5425  caovlem2d  6204  caofcom  6255  fnexALT  6262  tfr1onlemres  6501  tfrcllemres  6514  tfri3  6519  ixpexgg  6877  f1domg  6917  fundmfi  7115  f1ofi  7121  finacn  7397  archnqq  7615  nqpru  7750  ltaddpr  7795  1idsr  7966  addgt0sr  7973  suplocsrlempr  8005  gt0ap0  8784  ap0gt0  8798  mulgt1  9021  gt0div  9028  ge0div  9029  ltdiv2  9045  creur  9117  avgle1  9363  recnz  9551  qreccl  9849  xrrege0  10033  peano2fzor  10450  flqltnz  10519  flqdiv  10555  zmodcl  10578  frecuzrdgtcl  10646  frecuzrdgfunlem  10653  seqfveqg  10712  seq3fveq  10713  ser3mono  10721  seqsplitg  10723  seqcaopr2g  10728  iseqf1olemkle  10731  seq3f1olemqsumkj  10745  seq3f1olemqsumk  10746  seqf1oglem2  10754  seqf1og  10755  seq3id  10759  seq3z  10762  seqhomog  10764  le2sq2  10849  bcpasc  11000  fihasheqf1oi  11021  seq3coll  11077  wrdnval  11115  wrdsymb1  11121  lswcl  11135  ccatlid  11154  ccatass  11156  ccat1st1st  11188  lswccats1fst  11191  swrdlsw  11217  ccatswrd  11218  pfxtrcfvl  11245  pfxsuff1eqwrdeq  11247  ccatpfx  11249  pfx1  11251  pfxswrd  11254  pfxlswccat  11261  swrdccatin2  11277  pfxccatin12  11281  caucvgrelemcau  11507  caucvgre  11508  r19.2uz  11520  sqrtgt0  11561  xrmaxiflemval  11777  clim2ser  11864  clim2ser2  11865  climub  11871  serf0  11879  fsumf1o  11917  fisumss  11919  fsumcl2lem  11925  fsumsplit  11934  fsum2dlemstep  11961  fisumrev2  11973  fsumlessfi  11987  telfsumo  11993  fsumparts  11997  fsumiun  12004  binom1dif  12014  isumsplit  12018  isumrpcl  12021  isumlessdc  12023  explecnv  12032  cvgratnnlemmn  12052  cvgratz  12059  cvgratgt0  12060  mertenslemi1  12062  clim2prod  12066  clim2divap  12067  fprodseq  12110  fprodf1o  12115  prodssdc  12116  fprodssdc  12117  fprodsplitdc  12123  fprodeq0  12144  fprod2dlemstep  12149  ef0lem  12187  eftlub  12217  tanval3ap  12241  dvdssubr  12366  divalgmod  12454  bitsdc  12474  bitsp1  12478  divgcdnn  12512  algfx  12590  eucalgcvga  12596  lcmcllem  12605  lcmneg  12612  isprm6  12685  cncongrprm  12695  phimullem  12763  pcid  12863  pcgcd  12868  pcz  12871  4sqlem9  12925  4sqlem15  12944  4sqlem16  12945  imasex  13354  grpidd  13432  gsumress  13444  ismndd  13486  subsubm  13532  grpinvid1  13601  grpinvid2  13602  grplcan  13611  grpinvinv  13616  grpinvval2  13632  mulgass  13712  mulgpropdg  13717  subginv  13734  subgmulg  13741  issubg2m  13742  issubg4m  13746  subsubg  13750  eqger  13777  qusinv  13789  resghm  13813  conjsubgen  13831  rngrz  13925  isrngd  13932  ringidss  14008  isringd  14020  ringlz  14022  ringrz  14023  unitgrp  14096  0unit  14109  unitnegcl  14110  dvrass  14119  dvreq1  14122  dvrdir  14123  ringinvdv  14125  invrpropdg  14129  rhmunitinv  14158  issubrng2  14190  subsubrng  14194  subrg1  14211  issubrg2  14221  subsubrg  14225  lmod0vs  14301  lmodvs0  14302  lmodvneg1  14310  islss3  14359  lspsnsubg  14376  lspid  14377  lspssv  14378  lspidm  14381  lspsnneg  14400  sraval  14417  qus1  14506  zringmulg  14578  mulgrhm  14589  znidom  14637  tgcl  14754  tgclb  14755  tgss2  14769  ntrss3  14813  ntridm  14816  opnssneib  14846  ssnei2  14847  innei  14853  resttopon  14861  cnpnei  14909  cnntri  14914  lmss  14936  txcnp  14961  blpnfctr  15129  mopni2  15173  bdmopn  15194  climcncf  15274  ivthdec  15334  cnplimcim  15357  dvconst  15384  dvconstre  15386  dvef  15417  plymullem  15440  plycoeid3  15447  rpcxpneg  15597  abscxp  15605  sgmmul  15686  lgscllem  15702  lgsvalmod  15714  lgsdir2  15728  lgsquadlem2  15773  lgsquad2lem2  15777  upgredg  15958  usgruspgrben  16000  usgredg3  16028  cvgcmp2nlemabs  16488  trilpolemisumle  16494  trilpolemeq1  16496  trilpolemlt1  16497  nconstwlpolemgt0  16520  neapmkvlem  16523