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  973  stoic2a  1478  sbcied2  3089  csbied2  3195  elpw2g  4287  pofun  4452  tfi  4724  fnbr  5480  caovlem2d  6272  caofcom  6323  fnexALT  6330  elabreximd  6346  tfr1onlemres  6610  tfrcllemres  6623  tfri3  6628  ixpexgg  6994  f1domg  7034  fundmfi  7241  f1ofi  7247  finacn  7550  archnqq  7774  nqpru  7909  ltaddpr  7954  1idsr  8125  addgt0sr  8132  suplocsrlempr  8164  gt0ap0  8944  ap0gt0  8958  mulgt1  9183  gt0div  9190  ge0div  9191  ltdiv2  9207  creur  9279  avgle1  9525  recnz  9718  qreccl  10021  xrrege0  10206  peano2fzor  10628  flqltnz  10700  flqdiv  10736  zmodcl  10759  frecuzrdgtcl  10827  frecuzrdgfunlem  10834  seqfveqg  10893  seq3fveq  10894  ser3mono  10902  seqsplitg  10904  seqcaopr2g  10909  iseqf1olemkle  10912  seq3f1olemqsumkj  10926  seq3f1olemqsumk  10927  seqf1oglem2  10935  seqf1og  10936  seq3id  10940  seq3z  10943  seqhomog  10945  le2sq2  11030  bcpasc  11182  fihasheqf1oi  11204  seq3coll  11272  wrdnval  11313  wrdsymb1  11319  lswcl  11333  ccatlid  11352  ccatass  11354  ccat1st1st  11387  lswccats1fst  11390  swrdlsw  11419  ccatswrd  11420  pfxtrcfvl  11447  pfxsuff1eqwrdeq  11449  ccatpfx  11451  pfx1  11453  pfxswrd  11456  pfxlswccat  11463  swrdccatin2  11479  pfxccatin12  11483  caucvgrelemcau  11724  caucvgre  11725  r19.2uz  11737  sqrtgt0  11778  xrmaxiflemval  11994  clim2ser  12081  clim2ser2  12082  climub  12088  serf0  12096  fsumf1o  12135  fisumss  12137  fsumcl2lem  12143  fsumsplit  12152  fsum2dlemstep  12179  fisumrev2  12191  fsumlessfi  12205  telfsumo  12211  fsumparts  12215  fsumiun  12222  binom1dif  12232  isumsplit  12236  isumrpcl  12239  isumlessdc  12241  explecnv  12250  cvgratnnlemmn  12270  cvgratz  12277  cvgratgt0  12278  mertenslemi1  12280  clim2prod  12284  clim2divap  12285  fprodseq  12328  fprodf1o  12333  prodssdc  12334  fprodssdc  12335  fprodsplitdc  12341  fprodeq0  12362  fprod2dlemstep  12367  ef0lem  12405  eftlub  12435  tanval3ap  12459  dvdssubr  12584  divalgmod  12672  bitsdc  12692  bitsp1  12696  divgcdnn  12730  algfx  12808  eucalgcvga  12814  lcmcllem  12823  lcmneg  12830  isprm6  12903  cncongrprm  12913  phimullem  12981  pcid  13081  pcgcd  13086  pcz  13089  4sqlem9  13143  4sqlem15  13162  4sqlem16  13163  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemsel1i  13234  ballotfilemsima  13237  ballotfilemfrceq  13250  imasex  13603  grpidd  13680  gzsumress  13689  ismndd  13727  subsubm  13767  grpinvid1  13834  grpinvid2  13835  grplcan  13844  grpinvinv  13849  grpinvval2  13865  mulgass  13939  mulgpropdg  13944  subginv  13961  subgmulg  13968  issubg2m  13969  issubg4m  13973  subsubg  13977  eqger  14004  qusinv  14016  resghm  14040  conjsubgen  14058  rngrz  14220  isrngd  14227  ringidss  14307  isringd  14319  ringlz  14321  ringrz  14322  unitgrp  14396  0unit  14409  unitnegcl  14410  dvrass  14419  dvreq1  14422  dvrdir  14423  ringinvdv  14425  invrpropdg  14429  rhmunitinv  14458  issubrng2  14491  subsubrng  14495  subrg1  14512  issubrg2  14522  subsubrg  14526  lmod0vs  14630  lmodvs0  14631  lmodvneg1  14639  islss3  14688  lspsnsubg  14705  lspid  14706  lspssv  14707  lspidm  14710  lspsnneg  14729  sraval  14746  qus1  14835  zringmulg  14905  mulgrhm  14916  znidom  14964  tgcl  15088  tgclb  15089  tgss2  15103  ntrss3  15147  ntridm  15150  opnssneib  15180  ssnei2  15181  innei  15187  resttopon  15195  cnpnei  15243  cnntri  15248  lmss  15270  txcnp  15295  blpnfctr  15463  mopni2  15507  bdmopn  15528  climcncf  15608  ivthdec  15668  cnplimcim  15691  dvconst  15718  dvconstre  15720  dvef  15751  plymullem  15774  plycoeid3  15781  rpcxpneg  15932  abscxp  15940  sgmmul  16024  lgscllem  16040  lgsvalmod  16052  lgsdir2  16066  lgsquadlem2  16111  lgsquad2lem2  16115  upgredg  16299  usgruspgrben  16341  usgredg3  16369  cvgcmp2nlemabs  16986  trilpolemisumle  16992  trilpolemeq1  16994  trilpolemlt1  16995  nconstwlpolemgt0  17019  neapmkvlem  17022