MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syldan Structured version   Unicode version

Theorem syldan 470
Description: A syllogism deduction with conjoined antecedents. (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
StepHypRef Expression
1 syldan.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
2 syldan.2 . . . 4  |-  ( (
ph  /\  ch )  ->  th )
32expcom 435 . . 3  |-  ( ch 
->  ( ph  ->  th )
)
43adantrd 468 . 2  |-  ( ch 
->  ( ( ph  /\  ps )  ->  th )
)
51, 4mpcom 36 1  |-  ( (
ph  /\  ps )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  sylan2  474  thema2a  1582  sbcied2  3322  csbied2  3413  elpwunsn  4015  elpw2g  4553  pofun  4755  fnbr  5611  dffv2  5863  grprinvlem  6401  caofid0l  6448  caofid0r  6449  caofid1  6450  caofid2  6451  caofcom  6452  fnexALT  6643  frxp  6782  fnse  6789  brovex  6840  tfr3  6958  tz7.48-2  6997  oaf1o  7102  omlimcl  7117  oeeulem  7140  ixpexg  7387  f1domg  7429  domdifsn  7494  unxpdom2  7622  xpfir  7636  fofinf1o  7693  fofi  7698  imafi  7705  intrnfi  7767  ordtypelem6  7838  oiexg  7850  cantnfp1lem3  7989  cantnflem1  7998  cantnfp1lem3OLD  8015  cantnflem1OLD  8021  infxpenlem  8281  fseqenlem2  8296  ssnum  8310  acni2  8317  finacn  8321  fonum  8329  infpwfien  8333  inffien  8334  infunsdom1  8483  infunsdom  8484  ackbij1lem12  8501  cfslb2n  8538  fin23lem28  8610  compssiso  8644  isf34lem5  8648  fin56  8663  axcc3  8708  axdc3lem2  8721  ttukeylem6  8784  ttukeylem7  8785  brdom3  8796  gchdomtri  8897  fpwwe2lem13  8910  gchxpidm  8937  tsken  9022  tsksn  9028  tsk1  9032  tsk2  9033  2domtsk  9034  tskcard  9049  r1tskina  9050  gruss  9064  gruxp  9075  gruina  9086  grur1a  9087  ltaddpr  9304  ltexprlem7  9312  1idsr  9366  addgt0sr  9372  recexsr  9375  msqgt0  9961  mulgt1  10289  gt0div  10296  ge0div  10297  ltdiv2  10318  ltrec1  10320  lerec2  10321  lediv2  10323  lediv12a  10326  recreclt  10332  creur  10417  nn2ge  10448  avgle1  10665  recnz  10818  suprzcl  10822  uzwo2  11020  rpnnen1lem5  11084  xrrege0  11247  xlemul1a  11352  xrsupsslem  11370  xrinfmsslem  11371  supxr2  11377  supxrpnf  11382  supxrunb1  11383  supxrunb2  11384  ixxun  11417  peano2fzor  11733  ioopnfsup  11804  modcl  11813  modge0  11818  zmodcl  11828  seqcl  11927  seqf  11928  seqfveq  11931  sermono  11939  seqsplit  11940  seqcaopr2  11943  seqf1olem2  11947  seqf1o  11948  seqhomo  11954  seqz  11955  le2sq2  12042  faclbnd4lem3  12172  bcpasc  12198  hashgt0  12253  hashge2el2dif  12286  seqcoll  12318  seqcoll2  12319  wrdsymb1  12364  ccatlid  12386  ccatass  12388  swrdtrcfvl  12446  swrdlsw  12448  2swrd1eqwrdeq  12450  ccatswrd  12452  swrd0swrd  12457  swrdccatwrd  12464  wrdeqcats1  12470  wrdeqs1cat  12471  swrdccatin2  12480  revccat  12508  revrev  12509  sqrlem7  12840  resqrex  12842  sqrgt0  12850  leabs  12890  absmax  12919  r19.2uz  12941  lo1bdd2  13104  o1lo12  13118  rlimclim1  13125  lo1eq  13148  rlimeq  13149  rlimcn1  13168  rlimcn2  13170  rlimdiv  13225  rlimsqzlem  13228  clim2ser  13234  clim2ser2  13235  climub  13241  isercolllem1  13244  isercolllem3  13246  isercoll2  13248  climsup  13249  serf0  13260  iseraltlem1  13261  fsumf1o  13302  fsumss  13304  fsumsplit  13318  fsum2dlem  13339  fsumless  13361  fsumabs  13366  fsumtscopo  13367  fsumparts  13371  fsumrlim  13376  fsumo1  13377  o1fsum  13378  cvgcmp  13381  cvgcmpce  13383  fsumiun  13386  binom1dif  13398  incexclem  13401  incexc  13402  isumsplit  13405  isumrpcl  13408  isumless  13410  isumsup2  13411  isumltss  13413  climcnds  13416  supcvg  13420  expcnv  13428  explecnv  13429  geomulcvg  13438  cvgrat  13445  mertenslem1  13446  efcllem  13465  ef0lem  13466  eftlub  13495  tanval3  13520  tanneg  13534  rpnnen2lem7  13605  rpnnen2lem9  13607  rpnnen2lem11  13609  ruclem9  13622  dvdssubr  13676  divalgmod  13712  bitsf1  13744  algfx  13857  eucalgcvga  13863  isprm6  13897  phimullem  13956  eulerthlem2  13959  pcid  14041  pcgcd  14046  unbenlem  14071  prmreclem4  14082  prmreclem5  14083  4sqlem9  14109  4sqlem15  14122  4sqlem16  14123  vdwlem2  14145  vdwlem6  14149  vdwlem10  14153  vdwlem11  14154  vdwlem13  14156  ramval  14171  ressabs  14338  imasaddflem  14570  imasvscaf  14579  mrcid  14653  mrcidb  14655  mrcidm  14659  fucidcl  14977  setcmon  15057  setcepi  15058  catccatid  15072  xpccatid  15100  yonedalem4c  15189  yonedainv  15193  pospo  15245  latjlej1  15337  latmlem1  15353  latledi  15361  latj32  15369  latjjdi  15375  mrelatlub  15458  mreclatBAD  15459  psss  15486  tsrlemax  15492  grpidd  15545  ismndd  15546  issubmnd  15551  subsubm  15587  gsumress  15609  gsumval2  15615  grpinvid1  15688  grpinvid2  15689  grplcan  15692  grpinvinv  15695  grpinvval2  15711  mulgass  15759  mulgpropd  15762  subginv  15790  subgmulg  15797  issubg2  15798  issubg4  15802  subsubg  15806  eqger  15833  divsinv  15842  resghm  15865  pwsdiagghm  15876  conjsubgen  15881  conjnsg  15884  subgga  15920  gass  15921  gasubg  15922  orbstafun  15931  orbsta  15933  symgextfv  16025  psgnunilem5  16102  gexcl2  16192  gexdvds3  16193  sylow1lem2  16202  sylow2blem1  16223  pj1ghm  16304  frgpup1  16376  frgpup3lem  16378  cntzspan  16430  cyggeninv  16464  lt6abl  16475  cycsubgcyg  16481  gsumval3eu  16485  gsumval3OLD  16486  gsumval3  16489  gsumzres  16492  gsumzresOLD  16496  gsumzaddlem  16512  gsumzaddlemOLD  16514  gsumzsplit  16522  gsumzsplitOLD  16523  gsum2d  16568  gsum2dOLD  16569  gsum2d2lem  16570  dprdres  16630  dprdz  16632  dmdprdsplitlem  16639  dmdprdsplitlemOLD  16640  dprdcntz2  16641  dprddisj2  16642  dprddisj2OLD  16643  dprd2dlem1  16645  dmdprdsplit2lem  16649  dmdprdsplit2  16650  dprdsplit  16652  ablfac1c  16677  ablfac1eulem  16678  ablfac1eu  16679  pgpfac1lem2  16681  ablfac2  16695  rngidss  16777  isrngd  16785  rnglz  16787  rngrz  16788  gsumdixpOLD  16806  gsumdixp  16807  0unit  16878  unitnegcl  16879  rnginvdv  16892  invrpropd  16896  subrg1  16981  subrginv  16987  issubrg2  16991  subsubrg  16997  abvneg  17025  lmod0vs  17087  lmodvs0  17088  lmodvneg1  17094  islss3  17146  lspsnsubg  17167  lspidm  17173  lspsnneg  17193  lmhmlsp  17236  drngnidl  17417  psrass1lem  17553  psrlinv  17574  psrlidm  17580  psrlidmOLD  17581  mplsubglem  17617  mplsubglemOLD  17619  mplcoe1  17651  mplcoe5  17655  mplcoe2OLD  17657  mplind  17691  mpfind  17729  evls1val  17864  evls1rhm  17866  evl1sca  17877  xrsdsreval  17967  xrsdsreclb  17969  zringmulg  18000  zrngmulg  18006  mulgrhm  18035  mulgrhmOLD  18038  znfld  18102  cygznlem3  18111  remulg  18146  ocvlsp  18210  pjff  18246  pjf2  18248  pjfo  18249  ocvpj  18251  ishil2  18253  frlmsslsp  18332  frlmsslspOLD  18333  islinds2  18351  f1lindf  18360  mdet0pr  18514  m2detleib  18553  tgcl  18690  tgclb  18691  tgss2  18708  tgfiss  18712  opncld  18753  ntrval2  18771  ntrss3  18780  clsidm  18787  ntridm  18788  opnssneib  18835  ssnei2  18836  neindisj  18837  opnnei  18840  innei  18845  resttopon  18881  restcld  18892  restcls  18901  restntr  18902  perfopn  18905  cnpnei  18984  cncls2i  18990  cnntri  18991  cnclsi  18992  lmss  19018  pnrmopn  19063  lpcls  19084  perfcls  19085  cncmp  19111  cmpsublem  19118  cmpsub  19119  consuba  19140  clscon  19150  1stcrest  19173  lly1stc  19216  hauspwdom  19221  llycmpkgen2  19239  ptclsg  19304  txcnp  19309  txcmplem1  19330  xkococnlem  19348  qtoptopon  19393  qtopid  19394  kqopn  19423  ptunhmeo  19497  trfbas2  19532  trfbas  19533  filin  19543  filintn0  19550  trfil2  19576  fgtr  19579  trufil  19599  cfinufil  19617  elfm3  19639  fmfnfmlem4  19646  neiflim  19663  flfval  19679  flfnei  19680  fclsbas  19710  ptcmplem5  19744  cnextf  19754  cnextfres  19756  tgplacthmeo  19790  tgpconcompeqg  19798  tgpconcomp  19799  tsmssubm  19832  tsmssplit  19842  tsmsxplem1  19843  restutopopn  19929  isucn2  19970  cnextucn  19994  blpnfctr  20127  mopni2  20184  stdbdmopn  20209  met1stc  20212  metutopOLD  20273  psmetutop  20274  nrmmetd  20283  tngngp2  20354  xrsxmet  20502  metdsle  20544  climcncf  20592  icoopnst  20627  iocopnst  20628  cnheibor  20643  bndth  20646  htpyco1  20666  htpyco2  20667  phtpyco2  20678  pi1xfr  20743  pi1coghm  20749  lmmbrf  20889  lmnn  20890  caucfil  20910  cmetcaulem  20915  iscmet3  20920  cfilresi  20922  caussi  20924  causs  20925  lmle  20928  lmclimf  20930  bcthlem4  20954  bcth3  20958  rrxnm  21011  rrxcph  21012  rrxmval  21020  rrxmetlem  21022  rrxmet  21023  rrxdstprj1  21024  minveclem4  21035  ivth2  21055  ivthicc  21058  cniccbdd  21061  ovollb2  21088  ovolctb  21089  ovolunlem1a  21095  ovolunlem1  21096  ovolshftlem1  21108  ovolicc2lem1  21116  ovolicc2lem2  21117  ovolicc2lem4  21119  ovolicc2lem5  21120  uniioombllem2  21179  uniioombllem3  21181  volivth  21203  mbfss  21240  mbflimsup  21260  itg1val2  21278  i1fadd  21289  i1fmul  21290  itg1addlem4  21293  i1fmulc  21297  itg1mulc  21298  mbfi1fseqlem4  21312  itg2const2  21335  itg2seq  21336  itg2splitlem  21342  itg2split  21343  itg2addlem  21352  itg2gt0  21354  itg2cnlem2  21356  iblss  21398  iblss2  21399  itgss3  21408  itgless  21410  itgfsum  21420  itgsplit  21429  itgsplitioo  21431  itgcn  21436  ditgcl  21449  ditgswap  21450  ditgsplitlem  21451  dvconst  21507  dvaddbr  21528  dvmulbr  21529  rolle  21578  dvlip  21581  dvlipcn  21582  dvlip2  21583  dveq0  21588  dv11cn  21589  dvivthlem1  21596  dvne0  21599  lhop1lem  21601  lhop2  21603  lhop  21604  dvcnvre  21607  dvfsumle  21609  dvfsumge  21610  dvfsumabs  21611  dvfsumlem2  21615  dvfsumlem3  21616  dvfsumrlimge0  21618  dvfsumrlim  21619  ftc1lem1  21623  ftc1lem4  21627  ftc1lem5  21628  itgsubstlem  21636  deg1sclle  21700  uc1pmon1p  21739  plymullem  21800  coeeulem  21808  dgrlem  21813  dgrlb  21820  coemulhi  21837  dgrcolem2  21857  plydiveu  21880  vieta1lem2  21893  vieta1  21894  taylplem1  21944  taylplem2  21945  dvtaylp  21951  taylthlem1  21954  taylthlem2  21955  ulmdvlem1  21981  mtest  21985  radcnv0  21997  pserulm  22003  pserdvlem2  22009  abelthlem3  22014  abelthlem5  22016  abelthlem7  22019  efcvx  22030  sineq0  22099  tanord  22110  tanregt0  22111  logne0  22167  argregt0  22175  argimgt0  22177  argimlt0  22178  logneg2  22180  logcnlem3  22205  cxpsqr  22264  loglesqr  22312  ang180lem2  22322  isosctrlem1  22332  dcubic  22357  atanlogaddlem  22424  atanlogsub  22427  atantan  22434  atans2  22442  log2tlbnd  22456  birthdaylem2  22462  rlimcnp  22475  efrlim  22479  jensenlem1  22496  jensenlem2  22497  jensen  22498  fsumharmonic  22521  wilthlem2  22523  ftalem4  22529  ftalem5  22530  basellem3  22536  basellem4  22537  ppisval  22557  chtdif  22612  dvdsflsumcom  22644  musumsum  22648  muinv  22649  sgmmul  22656  chtleppi  22665  chtublem  22666  fsumvma  22668  chpval2  22673  chpub  22675  bposlem3  22741  lgsvalmod  22770  lgsdir2  22783  lgsdchr  22803  lgsquadlem2  22810  lgsquad2lem2  22814  chebbnd1lem1  22834  chebbnd1lem3  22836  dchrisumlem1  22854  dchrisumlem2  22855  dchrisumlem3  22856  dchrisum0fno1  22876  rpvmasum2  22877  dchrisum0lem1b  22880  dchrisum0lem1  22881  mulog2sumlem2  22900  chpdifbndlem1  22918  pntrsumbnd2  22932  pntrlog2bndlem6  22948  pntpbnd1  22951  pntlemj  22968  pntlemf  22970  qabvle  22990  padicabv  22995  padicabvcxp  22997  ostth2lem3  23000  ttgval  23256  colinearalg  23291  axcontlem2  23346  axcontlem7  23351  usgraedg3  23439  usgrarnedg1  23442  fargshiftfo  23659  grpoidinvlem2  23827  grpoidinvlem3  23828  grpoideu  23831  grpoinvid1  23852  grpoinvid2  23853  grpolcan  23855  grpo2inv  23861  grpoinvop  23863  grpomuldivass  23871  grpopnpcan2  23875  grponnncan2  23876  grponpncan  23877  gxinv  23892  gxid  23895  ablo4  23909  ablomuldiv  23911  ablodivdiv4  23913  ablonnncan  23915  ablonnncan1  23917  ghgrplem1  23988  ghgrp  23990  ghablo  23991  ghsubgolem  23992  rngolz  24023  rngorz  24024  vc0  24082  vcz  24083  nvzs  24160  nvmdi  24165  nvnegneg  24166  nvsubadd  24170  nvnpcan  24175  nvmeq0  24179  nvabs  24196  nvelbl2  24220  sspmval  24266  sspz  24268  sspival  24271  sspimsval  24273  nmoub3i  24308  nmblolbii  24334  dipsubdir  24383  sspph  24390  ubthlem1  24406  minvecolem3  24412  minvecolem4  24416  htthlem  24454  hvaddsub4  24615  hi2eq  24642  shsel3  24853  pjpreeq  24936  pjeq  24937  chabs1  25054  pjspansn  25115  chscllem1  25175  chscllem2  25176  chscllem4  25178  5oalem2  25193  3oalem2  25201  pjoi0  25255  nmopub2tALT  25448  nmfnleub2  25465  eigvalcl  25500  eighmre  25502  leopmul  25673  nmopleid  25678  opsqrlem4  25682  spansncv2  25832  chcv1  25894  atcv0eq  25918  atexch  25920  chirredi  25933  cdj1i  25972  elabreximd  26026  iocinif  26205  ressmulgnn  26278  archirngz  26340  slmdvs0  26375  dvrdir  26392  rhmunitinv  26424  kerunit  26425  metider  26455  tpr2rico  26476  fsumcvg4  26514  lmdvg  26517  rezh  26534  qqhvq  26550  logbrec  26598  indsum  26613  indpreima  26615  indf1ofs  26616  esummono  26643  esumpcvgval  26661  esumpmono  26662  esumcvg  26669  sigaclfu2  26698  cldssbrsiga  26735  eulerpartlems  26877  eulerpartlemb  26885  eulerpartlemgvv  26893  eulerpartlemgs2  26897  probun  26936  ballotlemfc0  27009  ballotlemfcc  27010  ballotlemsel1i  27029  ballotlemsima  27032  ballotlemfrceq  27045  ballotlemirc  27048  sgnneg  27057  sgnmulrp2  27060  signsply0  27086  signslema  27097  signstf0  27103  signsvfn  27117  signsvfpn  27120  signsvfnn  27121  signshf  27123  dmlogdmgm  27144  subfacp1lem4  27205  subfacp1lem5  27206  erdszelem8  27220  ptpcon  27256  cvmliftmolem1  27304  cvmliftmolem2  27305  cvmliftlem6  27313  cvmliftlem7  27314  cvmliftlem10  27317  cvmlift2lem9  27334  cvmlift2lem11  27336  cvmlift2lem12  27337  ghomgsg  27446  ghomf1olem  27447  sinccvglem  27451  lediv2aALT  27456  rtrclreclem.trans  27482  clim2prod  27537  clim2div  27538  ntrivcvgfvn0  27548  ntrivcvgmullem  27550  fprodf1o  27593  prodss  27594  fprodss  27595  fprodser  27596  fprodsplit  27610  fprodeq0  27620  fprod2dlem  27625  binomfallfaclem2  27677  dfon2lem9  27738  sltval2  27931  outsideofeq  28295  lineelsb2  28313  bpolysum  28330  bpolydiflem  28331  onsuct0  28421  fin2so  28554  mblfinlem2  28567  voliunnfl  28573  volsupnfl  28574  dvtanlem  28579  itg2gt0cn  28585  itgaddnclem2  28589  bddiblnc  28600  ftc1cnnclem  28603  ftc1cnnc  28604  ftc1anclem2  28606  ftc1anclem5  28609  ftc1anclem6  28610  ftc1anclem7  28611  ftc1anclem8  28612  ftc1anc  28613  ftc2nc  28614  areacirc  28627  opnregcld  28663  isfne  28678  lfinpfin  28713  sdclem1  28777  fdc  28779  metf1o  28789  mettrifi  28791  equivtotbnd  28815  isbnd2  28820  bndss  28823  equivbnd2  28829  ismtyima  28840  ismtybndlem  28843  heiborlem1  28848  heiborlem8  28855  ismrer1  28875  ablo4pnp  28883  ghomdiv  28887  rngoneglmul  28895  rngonegrmul  28896  rngosubdi  28897  rngosubdir  28898  isdrngo2  28902  rngohomco  28918  rngoisoco  28926  iscringd  28937  crngm4  28941  idlsubcl  28961  divrngidl  28966  unichnidl  28969  keridl  28970  maxidln1  28982  maxidln0  28983  igenidl  29001  igenidl2  29003  ispridlc  29008  dmncan1  29014  elrfirn2  29170  2rexfrabdioph  29272  3rexfrabdioph  29273  4rexfrabdioph  29274  6rexfrabdioph  29275  7rexfrabdioph  29276  elnn0rabdioph  29279  irrapxlem5  29305  pell14qrre  29336  pell14qrne0  29337  pell14qrmulcl  29342  pellfundex  29365  monotoddzzfi  29421  jm2.17c  29443  fnwe2lem2  29542  flcidc  29669  itgpowd  29728  expgrowthi  29745  rfcnpre1  29879  rfcnpre2  29891  fmulcl  29900  fmul01lt1lem1  29903  fmul01lt1lem2  29904  climinf  29917  stoweidlem11  29944  stoweidlem14  29947  stoweidlem20  29953  stoweidlem26  29959  stoweidlem27  29960  stoweidlem31  29964  stoweidlem48  29981  stoweidlem51  29984  fsummsnunz  30379  wwlkm1edg  30505  clwlkisclwwlklem2a  30585  clwlkisclwwlk  30589  wrdnval  30612  wlkp1lenfislenp  30650  frgrareg  30848  pgrpgt2nabel  30909  invginvrid  30910  01eq0rng  30915  fsfnn0gsumfsffz  30944  lincsumscmcl  31074  mply1topmatval  31251  cpmadumatpolylem2  31336  onetansqsecsq  31392  bnj594  32205  riotasv3d  32917  lssats  32963  lfl0  33016  lfladdcl  33022  lflvscl  33028  lkr0f  33045  olm11  33178  latm12  33181  cvrle  33229  cvrnle  33231  cvrne  33232  cvrval3  33363  atcvrj0  33378  atltcvr  33385  atbtwnexOLDN  33397  atbtwnex  33398  3at  33440  2atneat  33465  llncvrlpln2  33507  lplncvrlvol2  33565  dalemdnee  33616  linepsubN  33702  isline2  33724  paddasslem17  33786  pmodN  33800  pmapjlln1  33805  pclidN  33846  polval2N  33856  polssatN  33858  polpmapN  33862  2polpmapN  33863  2polvalN  33864  2polssN  33865  3polN  33866  pclss2polN  33871  2pmaplubN  33876  polatN  33881  2polatN  33882  psubclsubN  33890  pmapidclN  33892  ispsubcl2N  33897  linepsubclN  33901  polsubclN  33902  lhpoc2N  33965  ltrnlaut  34073  ltrncnv  34096  cdlemc3  34143  cdleme3b  34179  cdleme42ke  34435  trlcoat  34673  tendoid  34723  tendoex  34925  dvalveclem  34976  diaintclN  35009  diasslssN  35010  dvhgrp  35058  dvhlveclem  35059  docaclN  35075  diaocN  35076  doca2N  35077  doca3N  35078  dvadiaN  35079  djaclN  35087  djajN  35088  dibval2  35095  dibvalrel  35114  dibintclN  35118  dicvalrelN  35136  xihopellsmN  35205  dihopellsm  35206  dihsslss  35227  dih1  35237  dih1dimatlem  35280  dihlspsnat  35284  dihintcl  35295  dihmeetcl  35296  dochval2  35303  dochcl  35304  dochlss  35305  dochssv  35306  dochvalr  35308  dochvalr2  35313  dochocss  35317  dochoc  35318  dochnoncon  35342  djhcl  35351  djhlj  35352  djhexmid  35362  dvh3dim3N  35400  lcfrlem21  35514  hlhilhillem  35914
  Copyright terms: Public domain W3C validator