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  4273  pofun  4438  tfi  4709  fnbr  5465  caovlem2d  6255  caofcom  6306  fnexALT  6313  elabreximd  6329  tfr1onlemres  6593  tfrcllemres  6606  tfri3  6611  ixpexgg  6970  f1domg  7010  fundmfi  7217  f1ofi  7223  finacn  7524  archnqq  7748  nqpru  7883  ltaddpr  7928  1idsr  8099  addgt0sr  8106  suplocsrlempr  8138  gt0ap0  8917  ap0gt0  8931  mulgt1  9154  gt0div  9161  ge0div  9162  ltdiv2  9178  creur  9250  avgle1  9496  recnz  9689  qreccl  9992  xrrege0  10177  peano2fzor  10599  flqltnz  10671  flqdiv  10707  zmodcl  10730  frecuzrdgtcl  10798  frecuzrdgfunlem  10805  seqfveqg  10864  seq3fveq  10865  ser3mono  10873  seqsplitg  10875  seqcaopr2g  10880  iseqf1olemkle  10883  seq3f1olemqsumkj  10897  seq3f1olemqsumk  10898  seqf1oglem2  10906  seqf1og  10907  seq3id  10911  seq3z  10914  seqhomog  10916  le2sq2  11001  bcpasc  11153  fihasheqf1oi  11175  seq3coll  11239  wrdnval  11280  wrdsymb1  11286  lswcl  11300  ccatlid  11319  ccatass  11321  ccat1st1st  11354  lswccats1fst  11357  swrdlsw  11386  ccatswrd  11387  pfxtrcfvl  11414  pfxsuff1eqwrdeq  11416  ccatpfx  11418  pfx1  11420  pfxswrd  11423  pfxlswccat  11430  swrdccatin2  11446  pfxccatin12  11450  caucvgrelemcau  11690  caucvgre  11691  r19.2uz  11703  sqrtgt0  11744  xrmaxiflemval  11960  clim2ser  12047  clim2ser2  12048  climub  12054  serf0  12062  fsumf1o  12101  fisumss  12103  fsumcl2lem  12109  fsumsplit  12118  fsum2dlemstep  12145  fisumrev2  12157  fsumlessfi  12171  telfsumo  12177  fsumparts  12181  fsumiun  12188  binom1dif  12198  isumsplit  12202  isumrpcl  12205  isumlessdc  12207  explecnv  12216  cvgratnnlemmn  12236  cvgratz  12243  cvgratgt0  12244  mertenslemi1  12246  clim2prod  12250  clim2divap  12251  fprodseq  12294  fprodf1o  12299  prodssdc  12300  fprodssdc  12301  fprodsplitdc  12307  fprodeq0  12328  fprod2dlemstep  12333  ef0lem  12371  eftlub  12401  tanval3ap  12425  dvdssubr  12550  divalgmod  12638  bitsdc  12658  bitsp1  12662  divgcdnn  12696  algfx  12774  eucalgcvga  12780  lcmcllem  12789  lcmneg  12796  isprm6  12869  cncongrprm  12879  phimullem  12947  pcid  13047  pcgcd  13052  pcz  13055  4sqlem9  13109  4sqlem15  13128  4sqlem16  13129  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemsel1i  13200  ballotfilemsima  13203  ballotfilemfrceq  13216  imasex  13569  grpidd  13646  gsumress  13658  ismndd  13698  subsubm  13738  grpinvid1  13807  grpinvid2  13808  grplcan  13817  grpinvinv  13822  grpinvval2  13838  mulgass  13912  mulgpropdg  13917  subginv  13934  subgmulg  13941  issubg2m  13942  issubg4m  13946  subsubg  13950  eqger  13977  qusinv  13989  resghm  14013  conjsubgen  14031  rngrz  14185  isrngd  14192  ringidss  14272  isringd  14284  ringlz  14286  ringrz  14287  unitgrp  14361  0unit  14374  unitnegcl  14375  dvrass  14384  dvreq1  14387  dvrdir  14388  ringinvdv  14390  invrpropdg  14394  rhmunitinv  14423  issubrng2  14456  subsubrng  14460  subrg1  14477  issubrg2  14487  subsubrg  14491  lmod0vs  14595  lmodvs0  14596  lmodvneg1  14604  islss3  14653  lspsnsubg  14670  lspid  14671  lspssv  14672  lspidm  14675  lspsnneg  14694  sraval  14711  qus1  14800  zringmulg  14872  mulgrhm  14883  znidom  14931  tgcl  15055  tgclb  15056  tgss2  15070  ntrss3  15114  ntridm  15117  opnssneib  15147  ssnei2  15148  innei  15154  resttopon  15162  cnpnei  15210  cnntri  15215  lmss  15237  txcnp  15262  blpnfctr  15430  mopni2  15474  bdmopn  15495  climcncf  15575  ivthdec  15635  cnplimcim  15658  dvconst  15685  dvconstre  15687  dvef  15718  plymullem  15741  plycoeid3  15748  rpcxpneg  15898  abscxp  15906  sgmmul  15990  lgscllem  16006  lgsvalmod  16018  lgsdir2  16032  lgsquadlem2  16077  lgsquad2lem2  16081  upgredg  16265  usgruspgrben  16307  usgredg3  16335  cvgcmp2nlemabs  16942  trilpolemisumle  16948  trilpolemeq1  16950  trilpolemlt1  16951  nconstwlpolemgt0  16976  neapmkvlem  16979