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

Theorem syldan 457
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 425 . . 3  |-  ( ch 
->  ( ph  ->  th )
)
43adantrd 455 . 2  |-  ( ch 
->  ( ( ph  /\  ps )  ->  th )
)
51, 4mpcom 34 1  |-  ( (
ph  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  sylan2  461  sbcied2  3158  csbied2  3254  elpw2g  4323  pofun  4479  elpwunsn  4716  fnbr  5506  dffv2  5755  fnexALT  5921  grprinvlem  6244  caofid0l  6291  caofid0r  6292  caofid1  6293  caofid2  6294  caofcom  6295  frxp  6415  fnse  6422  brovex  6433  riotasv3d  6557  tfr3  6619  tz7.48-2  6658  oaf1o  6765  omlimcl  6780  oeeulem  6803  ixpexg  7045  f1domg  7086  domdifsn  7150  unxpdom2  7276  xpfir  7290  fofinf1o  7346  fofi  7351  imafi  7357  intrnfi  7379  ordtypelem6  7448  oiexg  7460  cantnfp1lem3  7592  cantnflem1  7601  infxpenlem  7851  fseqenlem2  7862  ssnum  7876  acni2  7883  finacn  7887  fonum  7895  infpwfien  7899  inffien  7900  infunsdom1  8049  infunsdom  8050  ackbij1lem12  8067  cfslb2n  8104  fin23lem28  8176  compssiso  8210  isf34lem5  8214  fin56  8229  axcc3  8274  axdc3lem2  8287  ttukeylem6  8350  ttukeylem7  8351  brdom3  8362  gchdomtri  8460  fpwwe2lem13  8473  gchxpidm  8500  tsken  8585  tsksn  8591  tsk1  8595  tsk2  8596  2domtsk  8597  tskcard  8612  r1tskina  8613  gruss  8627  gruxp  8638  gruina  8649  grur1a  8650  ltaddpr  8867  ltexprlem7  8875  1idsr  8929  addgt0sr  8935  recexsr  8938  msqgt0  9504  mulgt1  9825  gt0div  9832  ge0div  9833  ltdiv2  9851  ltrec1  9853  lerec2  9854  lediv2  9856  lediv12a  9859  recreclt  9865  creur  9950  nn2ge  9981  avgle1  10163  recnz  10301  suprzcl  10305  uzwo2  10497  rpnnen1lem5  10560  xrrege0  10718  xlemul1a  10823  xrsupsslem  10841  xrinfmsslem  10842  supxr2  10848  supxrpnf  10853  supxrunb1  10854  supxrunb2  10855  ixxun  10888  peano2fzor  11149  ioopnfsup  11200  modcl  11208  modge0  11212  zmodcl  11221  seqcl  11298  seqf  11299  seqfveq  11302  sermono  11310  seqsplit  11311  seqcaopr2  11314  seqf1olem2  11318  seqf1o  11319  seqhomo  11325  seqz  11326  le2sq2  11412  faclbnd4lem3  11541  bcpasc  11567  hashgt0  11617  seqcoll  11667  seqcoll2  11668  ccatlid  11703  ccatass  11705  ccatswrd  11728  wrdeqcats1  11743  wrdeqs1cat  11744  revccat  11753  revrev  11754  sqrlem7  12009  resqrex  12011  sqrgt0  12019  leabs  12059  absmax  12088  r19.2uz  12110  lo1bdd2  12273  o1lo12  12287  rlimclim1  12294  lo1eq  12317  rlimeq  12318  rlimcn1  12337  rlimcn2  12339  rlimdiv  12394  rlimsqzlem  12397  clim2ser  12403  clim2ser2  12404  climub  12410  isercolllem1  12413  isercolllem3  12415  isercoll2  12417  climsup  12418  serf0  12429  iseraltlem1  12430  fsumf1o  12472  fsumss  12474  fsumsplit  12488  fsum2dlem  12509  fsumless  12530  fsumabs  12535  fsumtscopo  12536  fsumparts  12540  fsumrlim  12545  fsumo1  12546  o1fsum  12547  cvgcmp  12550  cvgcmpce  12552  fsumiun  12555  binom1dif  12567  incexclem  12571  incexc  12572  isumsplit  12575  isumrpcl  12578  isumless  12580  isumsup2  12581  isumltss  12583  climcnds  12586  supcvg  12590  expcnv  12598  explecnv  12599  geomulcvg  12608  cvgrat  12615  mertenslem1  12616  efcllem  12635  ef0lem  12636  eftlub  12665  tanval3  12690  tanneg  12704  rpnnen2lem7  12775  rpnnen2lem9  12777  rpnnen2lem11  12779  ruclem9  12792  dvdssubr  12846  divalgmod  12881  bitsf1  12913  algfx  13026  eucalgcvga  13032  isprm6  13064  phimullem  13123  eulerthlem2  13126  pcid  13201  pcgcd  13206  unbenlem  13231  prmreclem4  13242  prmreclem5  13243  4sqlem9  13269  4sqlem15  13282  4sqlem16  13283  vdwlem2  13305  vdwlem6  13309  vdwlem10  13313  vdwlem11  13314  vdwlem13  13316  ramval  13331  ressabs  13482  imasaddflem  13710  imasvscaf  13719  mrcid  13793  mrcidb  13795  mrcidm  13799  fucidcl  14117  setcmon  14197  setcepi  14198  catccatid  14212  xpccatid  14240  yonedalem4c  14329  yonedainv  14333  pospo  14385  latjlej1  14449  latmlem1  14465  latledi  14473  latj32  14481  latjjdi  14487  mrelatlub  14567  mreclat  14568  psss  14601  tsrlemax  14607  spwpr4c  14619  grpidd  14673  ismndd  14674  issubmnd  14679  subsubm  14712  gsumress  14732  gsumval2  14738  grpinvid1  14808  grpinvid2  14809  grplcan  14812  grpinvinv  14813  grpinvval2  14827  mulgass  14875  mulgpropd  14878  subginv  14906  subgmulg  14913  issubg2  14914  issubg4  14916  subsubg  14918  eqger  14945  divsinv  14954  resghm  14977  pwsdiagghm  14988  conjsubgen  14993  conjnsg  14996  subgga  15032  gass  15033  gasubg  15034  orbstafun  15043  orbsta  15045  gexcl2  15178  gexdvds3  15179  sylow1lem2  15188  sylow2blem1  15209  pj1ghm  15290  frgpup1  15362  frgpup3lem  15364  cntzspan  15415  cyggeninv  15448  lt6abl  15459  cycsubgcyg  15465  gsumval3eu  15468  gsumval3  15469  gsumzres  15472  gsumzaddlem  15481  gsumzsplit  15484  gsum2d  15501  gsum2d2lem  15502  dprdres  15541  dprdz  15543  dmdprdsplitlem  15550  dprdcntz2  15551  dprddisj2  15552  dprd2dlem1  15554  dmdprdsplit2lem  15558  dmdprdsplit2  15559  dprdsplit  15561  ablfac1c  15584  ablfac1eulem  15585  ablfac1eu  15586  pgpfac1lem2  15588  ablfac2  15602  rngidss  15645  isrngd  15653  rnglz  15655  rngrz  15656  gsumdixp  15670  0unit  15740  unitnegcl  15741  rnginvdv  15754  invrpropd  15758  subrg1  15833  subrginv  15839  issubrg2  15843  subsubrg  15849  abvneg  15877  lmod0vs  15938  lmodvs0  15939  lmodvneg1  15942  islss3  15990  lspsnsubg  16011  lspidm  16017  lspsnneg  16037  lmhmlsp  16080  drngnidl  16255  psrass1lem  16397  psrlinv  16416  psrlidm  16422  mplsubglem  16453  mplcoe1  16483  mplcoe2  16485  mplind  16517  xrsdsreval  16698  xrsdsreclb  16700  mulgrhm  16742  znfld  16796  cygznlem3  16805  ocvlsp  16858  pjff  16894  pjf2  16896  pjfo  16897  ocvpj  16899  ishil2  16901  tgcl  16989  tgclb  16990  tgss2  17007  tgfiss  17011  opncld  17052  ntrval2  17070  ntrss3  17079  clsidm  17086  ntridm  17087  opnssneib  17134  ssnei2  17135  neindisj  17136  opnnei  17139  innei  17144  resttopon  17179  restcld  17190  restcls  17199  restntr  17200  perfopn  17203  cnpnei  17282  cncls2i  17288  cnntri  17289  cnclsi  17290  lmss  17316  pnrmopn  17361  lpcls  17382  perfcls  17383  cncmp  17409  cmpsublem  17416  cmpsub  17417  consuba  17436  clscon  17446  1stcrest  17469  lly1stc  17512  hauspwdom  17517  llycmpkgen2  17535  ptclsg  17600  txcnp  17605  txcmplem1  17626  xkococnlem  17644  qtoptopon  17689  qtopid  17690  kqopn  17719  ptunhmeo  17793  trfbas2  17828  trfbas  17829  filin  17839  filintn0  17846  trfil2  17872  fgtr  17875  trufil  17895  cfinufil  17913  elfm3  17935  fmfnfmlem4  17942  neiflim  17959  flfval  17975  flfnei  17976  fclsbas  18006  ptcmplem5  18040  cnextf  18050  cnextfres  18052  tgplacthmeo  18086  tgpconcompeqg  18094  tgpconcomp  18095  tsmssubm  18125  tsmssplit  18134  tsmsxplem1  18135  restutopopn  18221  isucn2  18262  cnextucn  18286  blpnfctr  18419  mopni2  18476  stdbdmopn  18501  met1stc  18504  metutopOLD  18565  psmetutop  18566  nrmmetd  18575  tngngp2  18646  xrsxmet  18793  metdsle  18835  climcncf  18883  icoopnst  18917  iocopnst  18918  cnheibor  18933  bndth  18936  htpyco1  18956  htpyco2  18957  phtpyco2  18968  pi1xfr  19033  pi1coghm  19039  lmmbrf  19168  lmnn  19169  caucfil  19189  cmetcaulem  19194  iscmet3  19199  cfilresi  19201  caussi  19203  causs  19204  lmle  19207  lmclimf  19209  bcthlem4  19233  bcth3  19237  minveclem4  19286  ivth2  19305  ivthicc  19308  cniccbdd  19311  ovollb2  19338  ovolctb  19339  ovolunlem1a  19345  ovolunlem1  19346  ovolshftlem1  19358  ovolicc2lem1  19366  ovolicc2lem2  19367  ovolicc2lem4  19369  ovolicc2lem5  19370  uniioombllem2  19428  uniioombllem3  19430  volivth  19452  mbfss  19491  mbflimsup  19511  itg1val2  19529  i1fadd  19540  i1fmul  19541  itg1addlem4  19544  i1fmulc  19548  itg1mulc  19549  mbfi1fseqlem4  19563  itg2const2  19586  itg2seq  19587  itg2splitlem  19593  itg2split  19594  itg2addlem  19603  itg2gt0  19605  itg2cnlem2  19607  iblss  19649  iblss2  19650  itgss3  19659  itgless  19661  itgfsum  19671  itgsplit  19680  itgsplitioo  19682  itgcn  19687  ditgcl  19698  ditgswap  19699  ditgsplitlem  19700  dvconst  19756  dvaddbr  19777  dvmulbr  19778  rolle  19827  dvlip  19830  dvlipcn  19831  dvlip2  19832  dveq0  19837  dv11cn  19838  dvivthlem1  19845  dvne0  19848  lhop1lem  19850  lhop2  19852  lhop  19853  dvcnvre  19856  dvfsumle  19858  dvfsumge  19859  dvfsumabs  19860  dvfsumlem2  19864  dvfsumlem3  19865  dvfsumrlimge0  19867  dvfsumrlim  19868  ftc1lem1  19872  ftc1lem4  19876  ftc1lem5  19877  itgsubstlem  19885  evl1sca  19903  mpfind  19918  deg1sclle  19988  uc1pmon1p  20027  plymullem  20088  coeeulem  20096  dgrlem  20101  dgrlb  20108  coemulhi  20125  dgrcolem2  20145  plydiveu  20168  vieta1lem2  20181  vieta1  20182  taylplem1  20232  taylplem2  20233  dvtaylp  20239  taylthlem1  20242  taylthlem2  20243  ulmdvlem1  20269  mtest  20273  radcnv0  20285  pserulm  20291  pserdvlem2  20297  abelthlem3  20302  abelthlem5  20304  abelthlem7  20307  efcvx  20318  sineq0  20382  tanord  20393  tanregt0  20394  logne0  20450  argregt0  20458  argimgt0  20460  argimlt0  20461  logneg2  20463  logcnlem3  20488  cxpsqr  20547  loglesqr  20595  ang180lem2  20605  isosctrlem1  20615  dcubic  20639  atanlogaddlem  20706  atanlogsub  20709  atantan  20716  atans2  20724  log2tlbnd  20738  birthdaylem2  20744  rlimcnp  20757  efrlim  20761  jensenlem1  20778  jensenlem2  20779  jensen  20780  fsumharmonic  20803  wilthlem2  20805  ftalem4  20811  ftalem5  20812  basellem3  20818  basellem4  20819  ppisval  20839  chtdif  20894  dvdsflsumcom  20926  musumsum  20930  muinv  20931  sgmmul  20938  chtleppi  20947  chtublem  20948  fsumvma  20950  chpval2  20955  chpub  20957  bposlem3  21023  lgsvalmod  21052  lgsdir2  21065  lgsdchr  21085  lgsquadlem2  21092  lgsquad2lem2  21096  chebbnd1lem1  21116  chebbnd1lem3  21118  dchrisumlem1  21136  dchrisumlem2  21137  dchrisumlem3  21138  dchrisum0fno1  21158  rpvmasum2  21159  dchrisum0lem1b  21162  dchrisum0lem1  21163  mulog2sumlem2  21182  chpdifbndlem1  21200  pntrsumbnd2  21214  pntrlog2bndlem6  21230  pntpbnd1  21233  pntlemj  21250  pntlemf  21252  qabvle  21272  padicabv  21277  padicabvcxp  21279  ostth2lem3  21282  usgraedg3  21358  usgrarnedg1  21361  fargshiftfo  21578  grpoidinvlem2  21746  grpoidinvlem3  21747  grpoideu  21750  grpoinvid1  21771  grpoinvid2  21772  grpolcan  21774  grpo2inv  21780  grpoinvop  21782  grpomuldivass  21790  grpopnpcan2  21794  grponnncan2  21795  grponpncan  21796  gxinv  21811  gxid  21814  ablo4  21828  ablomuldiv  21830  ablodivdiv4  21832  ablonnncan  21834  ablonnncan1  21836  ghgrplem1  21907  ghgrp  21909  ghablo  21910  ghsubgolem  21911  rngolz  21942  rngorz  21943  vc0  22001  vcz  22002  nvzs  22079  nvmdi  22084  nvnegneg  22085  nvsubadd  22089  nvnpcan  22094  nvmeq0  22098  nvabs  22115  nvelbl2  22139  sspmval  22185  sspz  22187  sspival  22190  sspimsval  22192  nmoub3i  22227  nmblolbii  22253  dipsubdir  22302  sspph  22309  ubthlem1  22325  minvecolem3  22331  minvecolem4  22335  htthlem  22373  hvaddsub4  22533  hi2eq  22560  shsel3  22770  pjpreeq  22853  pjeq  22854  chabs1  22971  pjspansn  23032  chscllem1  23092  chscllem2  23093  chscllem4  23095  5oalem2  23110  3oalem2  23118  pjoi0  23172  nmopub2tALT  23365  nmfnleub2  23382  eigvalcl  23417  eighmre  23419  leopmul  23590  nmopleid  23595  opsqrlem4  23599  spansncv2  23749  chcv1  23811  atcv0eq  23835  atexch  23837  chirredi  23850  cdj1i  23889  elabreximd  23944  abfmpeld  24019  iocinif  24097  ressmulgnn  24158  dvrdir  24179  rhmunitinv  24213  kerunit  24214  zzsmulg  24218  remulg  24223  metider  24242  tpr2rico  24263  lmdvg  24291  rezh  24308  qqhvq  24324  logbrec  24358  indsum  24373  indpreima  24375  indf1ofs  24376  esummono  24403  esumpcvgval  24421  esumpmono  24422  esumcvg  24429  sigaclfu2  24457  cldssbrsiga  24494  probun  24630  ballotlemfc0  24703  ballotlemfcc  24704  ballotlemsel1i  24723  ballotlemsima  24726  ballotlemfrceq  24739  ballotlemirc  24742  dmlogdmgm  24761  subfacp1lem4  24822  subfacp1lem5  24823  erdszelem8  24837  ptpcon  24873  cvmliftmolem1  24921  cvmliftmolem2  24922  cvmliftlem6  24930  cvmliftlem7  24931  cvmliftlem10  24934  cvmlift2lem9  24951  cvmlift2lem11  24953  cvmlift2lem12  24954  ghomgsg  25057  ghomf1olem  25058  sinccvglem  25062  lediv2aALT  25070  rtrclreclem.trans  25099  clim2prod  25169  clim2div  25170  ntrivcvgfvn0  25180  ntrivcvgmullem  25182  fprodf1o  25225  prodss  25226  fprodss  25227  fprodser  25228  fprodsplit  25242  fprodeq0  25252  fprod2dlem  25257  binomfallfaclem2  25307  dfon2lem9  25361  sltval2  25524  colinearalg  25753  axcontlem2  25808  axcontlem7  25813  outsideofeq  25968  lineelsb2  25986  bpolysum  26003  bpolydiflem  26004  onsuct0  26095  mblfinlem  26143  voliunnfl  26149  volsupnfl  26150  itg2gt0cn  26159  itgaddnclem2  26163  bddiblnc  26174  ftc1cnnclem  26177  ftc1cnnc  26178  areacirc  26187  opnregcld  26223  isfne  26238  lfinpfin  26273  sdclem1  26337  fdc  26339  metf1o  26351  mettrifi  26353  equivtotbnd  26377  isbnd2  26382  bndss  26385  equivbnd2  26391  ismtyima  26402  ismtybndlem  26405  heiborlem1  26410  heiborlem8  26417  ismrer1  26437  ablo4pnp  26445  ghomdiv  26449  rngoneglmul  26457  rngonegrmul  26458  rngosubdi  26459  rngosubdir  26460  isdrngo2  26464  rngohomco  26480  rngoisoco  26488  iscringd  26499  crngm4  26503  idlsubcl  26523  divrngidl  26528  unichnidl  26531  keridl  26532  maxidln1  26544  maxidln0  26545  igenidl  26563  igenidl2  26565  ispridlc  26570  dmncan1  26576  elrfirn2  26640  2rexfrabdioph  26746  3rexfrabdioph  26747  4rexfrabdioph  26748  6rexfrabdioph  26749  7rexfrabdioph  26750  elnn0rabdioph  26753  irrapxlem5  26779  pell14qrre  26810  pell14qrne0  26811  pell14qrmulcl  26816  pellfundex  26839  monotoddzzfi  26895  jm2.17c  26917  fnwe2lem2  27016  frlmsslsp  27116  islinds2  27151  f1lindf  27160  flcidc  27247  psgnunilem5  27285  expgrowthi  27418  rfcnpre1  27557  rfcnpre2  27569  fmulcl  27578  fmul01lt1lem1  27581  fmul01lt1lem2  27582  climinf  27599  stoweidlem11  27627  stoweidlem14  27630  stoweidlem20  27636  stoweidlem26  27642  stoweidlem27  27643  stoweidlem31  27647  stoweidlem48  27664  stoweidlem51  27667  onetansqsecsq  28218  bnj594  28989  lssats  29495  lfl0  29548  lfladdcl  29554  lflvscl  29560  lkr0f  29577  olm11  29710  latm12  29713  cvrle  29761  cvrnle  29763  cvrne  29764  cvrval3  29895  atcvrj0  29910  atltcvr  29917  atbtwnexOLDN  29929  atbtwnex  29930  3at  29972  2atneat  29997  llncvrlpln2  30039  lplncvrlvol2  30097  dalemdnee  30148  linepsubN  30234  isline2  30256  paddasslem17  30318  pmodN  30332  pmapjlln1  30337  pclidN  30378  polval2N  30388  polssatN  30390  polpmapN  30394  2polpmapN  30395  2polvalN  30396  2polssN  30397  3polN  30398  pclss2polN  30403  2pmaplubN  30408  polatN  30413  2polatN  30414  psubclsubN  30422  pmapidclN  30424  ispsubcl2N  30429  linepsubclN  30433  polsubclN  30434  lhpoc2N  30497  ltrnlaut  30605  ltrncnv  30628  cdlemc3  30675  cdleme3b  30711  cdleme42ke  30967  trlcoat  31205  tendoid  31255  tendoex  31457  dvalveclem  31508  diaintclN  31541  diasslssN  31542  dvhgrp  31590  dvhlveclem  31591  docaclN  31607  diaocN  31608  doca2N  31609  doca3N  31610  dvadiaN  31611  djaclN  31619  djajN  31620  dibval2  31627  dibvalrel  31646  dibintclN  31650  dicvalrelN  31668  xihopellsmN  31737  dihopellsm  31738  dihsslss  31759  dih1  31769  dih1dimatlem  31812  dihlspsnat  31816  dihintcl  31827  dihmeetcl  31828  dochval2  31835  dochcl  31836  dochlss  31837  dochssv  31838  dochvalr  31840  dochvalr2  31845  dochocss  31849  dochoc  31850  dochnoncon  31874  djhcl  31883  djhlj  31884  djhexmid  31894  dvh3dim3N  31932  lcfrlem21  32046  hlhilhillem  32446
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator