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  963  stoic2a  1449  sbcied2  3043  csbied2  3149  elpw2g  4216  pofun  4377  tfi  4648  fnbr  5397  caovlem2d  6162  caofcom  6212  fnexALT  6219  tfr1onlemres  6458  tfrcllemres  6471  tfri3  6476  ixpexgg  6832  f1domg  6872  fundmfi  7065  f1ofi  7071  finacn  7347  archnqq  7565  nqpru  7700  ltaddpr  7745  1idsr  7916  addgt0sr  7923  suplocsrlempr  7955  gt0ap0  8734  ap0gt0  8748  mulgt1  8971  gt0div  8978  ge0div  8979  ltdiv2  8995  creur  9067  avgle1  9313  recnz  9501  qreccl  9798  xrrege0  9982  peano2fzor  10398  flqltnz  10467  flqdiv  10503  zmodcl  10526  frecuzrdgtcl  10594  frecuzrdgfunlem  10601  seqfveqg  10660  seq3fveq  10661  ser3mono  10669  seqsplitg  10671  seqcaopr2g  10676  iseqf1olemkle  10679  seq3f1olemqsumkj  10693  seq3f1olemqsumk  10694  seqf1oglem2  10702  seqf1og  10703  seq3id  10707  seq3z  10710  seqhomog  10712  le2sq2  10797  bcpasc  10948  fihasheqf1oi  10969  seq3coll  11024  wrdnval  11061  wrdsymb1  11067  lswcl  11081  ccatlid  11100  ccatass  11102  ccat1st1st  11131  lswccats1fst  11134  swrdlsw  11160  ccatswrd  11161  pfxtrcfvl  11188  pfxsuff1eqwrdeq  11190  ccatpfx  11192  pfx1  11194  pfxswrd  11197  pfxlswccat  11204  swrdccatin2  11220  pfxccatin12  11224  caucvgrelemcau  11406  caucvgre  11407  r19.2uz  11419  sqrtgt0  11460  xrmaxiflemval  11676  clim2ser  11763  clim2ser2  11764  climub  11770  serf0  11778  fsumf1o  11816  fisumss  11818  fsumcl2lem  11824  fsumsplit  11833  fsum2dlemstep  11860  fisumrev2  11872  fsumlessfi  11886  telfsumo  11892  fsumparts  11896  fsumiun  11903  binom1dif  11913  isumsplit  11917  isumrpcl  11920  isumlessdc  11922  explecnv  11931  cvgratnnlemmn  11951  cvgratz  11958  cvgratgt0  11959  mertenslemi1  11961  clim2prod  11965  clim2divap  11966  fprodseq  12009  fprodf1o  12014  prodssdc  12015  fprodssdc  12016  fprodsplitdc  12022  fprodeq0  12043  fprod2dlemstep  12048  ef0lem  12086  eftlub  12116  tanval3ap  12140  dvdssubr  12265  divalgmod  12353  bitsdc  12373  bitsp1  12377  divgcdnn  12411  algfx  12489  eucalgcvga  12495  lcmcllem  12504  lcmneg  12511  isprm6  12584  cncongrprm  12594  phimullem  12662  pcid  12762  pcgcd  12767  pcz  12770  4sqlem9  12824  4sqlem15  12843  4sqlem16  12844  imasex  13252  grpidd  13330  gsumress  13342  ismndd  13384  subsubm  13430  grpinvid1  13499  grpinvid2  13500  grplcan  13509  grpinvinv  13514  grpinvval2  13530  mulgass  13610  mulgpropdg  13615  subginv  13632  subgmulg  13639  issubg2m  13640  issubg4m  13644  subsubg  13648  eqger  13675  qusinv  13687  resghm  13711  conjsubgen  13729  rngrz  13823  isrngd  13830  ringidss  13906  isringd  13918  ringlz  13920  ringrz  13921  unitgrp  13993  0unit  14006  unitnegcl  14007  dvrass  14016  dvreq1  14019  dvrdir  14020  ringinvdv  14022  invrpropdg  14026  rhmunitinv  14055  issubrng2  14087  subsubrng  14091  subrg1  14108  issubrg2  14118  subsubrg  14122  lmod0vs  14198  lmodvs0  14199  lmodvneg1  14207  islss3  14256  lspsnsubg  14273  lspid  14274  lspssv  14275  lspidm  14278  lspsnneg  14297  sraval  14314  qus1  14403  zringmulg  14475  mulgrhm  14486  znidom  14534  tgcl  14651  tgclb  14652  tgss2  14666  ntrss3  14710  ntridm  14713  opnssneib  14743  ssnei2  14744  innei  14750  resttopon  14758  cnpnei  14806  cnntri  14811  lmss  14833  txcnp  14858  blpnfctr  15026  mopni2  15070  bdmopn  15091  climcncf  15171  ivthdec  15231  cnplimcim  15254  dvconst  15281  dvconstre  15283  dvef  15314  plymullem  15337  plycoeid3  15344  rpcxpneg  15494  abscxp  15502  sgmmul  15583  lgscllem  15599  lgsvalmod  15611  lgsdir2  15625  lgsquadlem2  15670  lgsquad2lem2  15674  upgredg  15848  cvgcmp2nlemabs  16173  trilpolemisumle  16179  trilpolemeq1  16181  trilpolemlt1  16182  nconstwlpolemgt0  16205  neapmkvlem  16208