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  969  stoic2a  1474  sbcied2  3083  csbied2  3189  elpw2g  4274  pofun  4439  tfi  4711  fnbr  5467  caovlem2d  6257  caofcom  6308  fnexALT  6315  elabreximd  6331  tfr1onlemres  6595  tfrcllemres  6608  tfri3  6613  ixpexgg  6972  f1domg  7012  fundmfi  7219  f1ofi  7225  finacn  7526  archnqq  7750  nqpru  7885  ltaddpr  7930  1idsr  8101  addgt0sr  8108  suplocsrlempr  8140  gt0ap0  8920  ap0gt0  8934  mulgt1  9159  gt0div  9166  ge0div  9167  ltdiv2  9183  creur  9255  avgle1  9501  recnz  9694  qreccl  9997  xrrege0  10182  peano2fzor  10604  flqltnz  10676  flqdiv  10712  zmodcl  10735  frecuzrdgtcl  10803  frecuzrdgfunlem  10810  seqfveqg  10869  seq3fveq  10870  ser3mono  10878  seqsplitg  10880  seqcaopr2g  10885  iseqf1olemkle  10888  seq3f1olemqsumkj  10902  seq3f1olemqsumk  10903  seqf1oglem2  10911  seqf1og  10912  seq3id  10916  seq3z  10919  seqhomog  10921  le2sq2  11006  bcpasc  11158  fihasheqf1oi  11180  seq3coll  11244  wrdnval  11285  wrdsymb1  11291  lswcl  11305  ccatlid  11324  ccatass  11326  ccat1st1st  11359  lswccats1fst  11362  swrdlsw  11391  ccatswrd  11392  pfxtrcfvl  11419  pfxsuff1eqwrdeq  11421  ccatpfx  11423  pfx1  11425  pfxswrd  11428  pfxlswccat  11435  swrdccatin2  11451  pfxccatin12  11455  caucvgrelemcau  11696  caucvgre  11697  r19.2uz  11709  sqrtgt0  11750  xrmaxiflemval  11966  clim2ser  12053  clim2ser2  12054  climub  12060  serf0  12068  fsumf1o  12107  fisumss  12109  fsumcl2lem  12115  fsumsplit  12124  fsum2dlemstep  12151  fisumrev2  12163  fsumlessfi  12177  telfsumo  12183  fsumparts  12187  fsumiun  12194  binom1dif  12204  isumsplit  12208  isumrpcl  12211  isumlessdc  12213  explecnv  12222  cvgratnnlemmn  12242  cvgratz  12249  cvgratgt0  12250  mertenslemi1  12252  clim2prod  12256  clim2divap  12257  fprodseq  12300  fprodf1o  12305  prodssdc  12306  fprodssdc  12307  fprodsplitdc  12313  fprodeq0  12334  fprod2dlemstep  12339  ef0lem  12377  eftlub  12407  tanval3ap  12431  dvdssubr  12556  divalgmod  12644  bitsdc  12664  bitsp1  12668  divgcdnn  12702  algfx  12780  eucalgcvga  12786  lcmcllem  12795  lcmneg  12802  isprm6  12875  cncongrprm  12885  phimullem  12953  pcid  13053  pcgcd  13058  pcz  13061  4sqlem9  13115  4sqlem15  13134  4sqlem16  13135  ballotfilemfc0  13182  ballotfilemfcc  13183  ballotfilemsel1i  13206  ballotfilemsima  13209  ballotfilemfrceq  13222  imasex  13575  grpidd  13652  gzsumress  13661  ismndd  13699  subsubm  13739  grpinvid1  13806  grpinvid2  13807  grplcan  13816  grpinvinv  13821  grpinvval2  13837  mulgass  13911  mulgpropdg  13916  subginv  13933  subgmulg  13940  issubg2m  13941  issubg4m  13945  subsubg  13949  eqger  13976  qusinv  13988  resghm  14012  conjsubgen  14030  rngrz  14192  isrngd  14199  ringidss  14279  isringd  14291  ringlz  14293  ringrz  14294  unitgrp  14368  0unit  14381  unitnegcl  14382  dvrass  14391  dvreq1  14394  dvrdir  14395  ringinvdv  14397  invrpropdg  14401  rhmunitinv  14430  issubrng2  14463  subsubrng  14467  subrg1  14484  issubrg2  14494  subsubrg  14498  lmod0vs  14602  lmodvs0  14603  lmodvneg1  14611  islss3  14660  lspsnsubg  14677  lspid  14678  lspssv  14679  lspidm  14682  lspsnneg  14701  sraval  14718  qus1  14807  zringmulg  14877  mulgrhm  14888  znidom  14936  tgcl  15060  tgclb  15061  tgss2  15075  ntrss3  15119  ntridm  15122  opnssneib  15152  ssnei2  15153  innei  15159  resttopon  15167  cnpnei  15215  cnntri  15220  lmss  15242  txcnp  15267  blpnfctr  15435  mopni2  15479  bdmopn  15500  climcncf  15580  ivthdec  15640  cnplimcim  15663  dvconst  15690  dvconstre  15692  dvef  15723  plymullem  15746  plycoeid3  15753  rpcxpneg  15904  abscxp  15912  sgmmul  15996  lgscllem  16012  lgsvalmod  16024  lgsdir2  16038  lgsquadlem2  16083  lgsquad2lem2  16087  upgredg  16271  usgruspgrben  16313  usgredg3  16341  cvgcmp2nlemabs  16958  trilpolemisumle  16964  trilpolemeq1  16966  trilpolemlt1  16967  nconstwlpolemgt0  16991  neapmkvlem  16994