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  3067  csbied2  3173  elpw2g  4244  pofun  4407  tfi  4678  fnbr  5431  caovlem2d  6210  caofcom  6261  fnexALT  6268  tfr1onlemres  6510  tfrcllemres  6523  tfri3  6528  ixpexgg  6886  f1domg  6926  fundmfi  7127  f1ofi  7133  finacn  7409  archnqq  7627  nqpru  7762  ltaddpr  7807  1idsr  7978  addgt0sr  7985  suplocsrlempr  8017  gt0ap0  8796  ap0gt0  8810  mulgt1  9033  gt0div  9040  ge0div  9041  ltdiv2  9057  creur  9129  avgle1  9375  recnz  9563  qreccl  9866  xrrege0  10050  peano2fzor  10467  flqltnz  10537  flqdiv  10573  zmodcl  10596  frecuzrdgtcl  10664  frecuzrdgfunlem  10671  seqfveqg  10730  seq3fveq  10731  ser3mono  10739  seqsplitg  10741  seqcaopr2g  10746  iseqf1olemkle  10749  seq3f1olemqsumkj  10763  seq3f1olemqsumk  10764  seqf1oglem2  10772  seqf1og  10773  seq3id  10777  seq3z  10780  seqhomog  10782  le2sq2  10867  bcpasc  11018  fihasheqf1oi  11039  seq3coll  11096  wrdnval  11134  wrdsymb1  11140  lswcl  11154  ccatlid  11173  ccatass  11175  ccat1st1st  11208  lswccats1fst  11211  swrdlsw  11240  ccatswrd  11241  pfxtrcfvl  11268  pfxsuff1eqwrdeq  11270  ccatpfx  11272  pfx1  11274  pfxswrd  11277  pfxlswccat  11284  swrdccatin2  11300  pfxccatin12  11304  caucvgrelemcau  11531  caucvgre  11532  r19.2uz  11544  sqrtgt0  11585  xrmaxiflemval  11801  clim2ser  11888  clim2ser2  11889  climub  11895  serf0  11903  fsumf1o  11941  fisumss  11943  fsumcl2lem  11949  fsumsplit  11958  fsum2dlemstep  11985  fisumrev2  11997  fsumlessfi  12011  telfsumo  12017  fsumparts  12021  fsumiun  12028  binom1dif  12038  isumsplit  12042  isumrpcl  12045  isumlessdc  12047  explecnv  12056  cvgratnnlemmn  12076  cvgratz  12083  cvgratgt0  12084  mertenslemi1  12086  clim2prod  12090  clim2divap  12091  fprodseq  12134  fprodf1o  12139  prodssdc  12140  fprodssdc  12141  fprodsplitdc  12147  fprodeq0  12168  fprod2dlemstep  12173  ef0lem  12211  eftlub  12241  tanval3ap  12265  dvdssubr  12390  divalgmod  12478  bitsdc  12498  bitsp1  12502  divgcdnn  12536  algfx  12614  eucalgcvga  12620  lcmcllem  12629  lcmneg  12636  isprm6  12709  cncongrprm  12719  phimullem  12787  pcid  12887  pcgcd  12892  pcz  12895  4sqlem9  12949  4sqlem15  12968  4sqlem16  12969  imasex  13378  grpidd  13456  gsumress  13468  ismndd  13510  subsubm  13556  grpinvid1  13625  grpinvid2  13626  grplcan  13635  grpinvinv  13640  grpinvval2  13656  mulgass  13736  mulgpropdg  13741  subginv  13758  subgmulg  13765  issubg2m  13766  issubg4m  13770  subsubg  13774  eqger  13801  qusinv  13813  resghm  13837  conjsubgen  13855  rngrz  13949  isrngd  13956  ringidss  14032  isringd  14044  ringlz  14046  ringrz  14047  unitgrp  14120  0unit  14133  unitnegcl  14134  dvrass  14143  dvreq1  14146  dvrdir  14147  ringinvdv  14149  invrpropdg  14153  rhmunitinv  14182  issubrng2  14214  subsubrng  14218  subrg1  14235  issubrg2  14245  subsubrg  14249  lmod0vs  14325  lmodvs0  14326  lmodvneg1  14334  islss3  14383  lspsnsubg  14400  lspid  14401  lspssv  14402  lspidm  14405  lspsnneg  14424  sraval  14441  qus1  14530  zringmulg  14602  mulgrhm  14613  znidom  14661  tgcl  14778  tgclb  14779  tgss2  14793  ntrss3  14837  ntridm  14840  opnssneib  14870  ssnei2  14871  innei  14877  resttopon  14885  cnpnei  14933  cnntri  14938  lmss  14960  txcnp  14985  blpnfctr  15153  mopni2  15197  bdmopn  15218  climcncf  15298  ivthdec  15358  cnplimcim  15381  dvconst  15408  dvconstre  15410  dvef  15441  plymullem  15464  plycoeid3  15471  rpcxpneg  15621  abscxp  15629  sgmmul  15710  lgscllem  15726  lgsvalmod  15738  lgsdir2  15752  lgsquadlem2  15797  lgsquad2lem2  15801  upgredg  15983  usgruspgrben  16025  usgredg3  16053  cvgcmp2nlemabs  16572  trilpolemisumle  16578  trilpolemeq1  16580  trilpolemlt1  16581  nconstwlpolemgt0  16604  neapmkvlem  16607