MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syldan Structured version   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  3190  csbied2  3286  elpw2g  4355  pofun  4511  elpwunsn  4749  fnbr  5539  dffv2  5788  fnexALT  5954  grprinvlem  6277  caofid0l  6324  caofid0r  6325  caofid1  6326  caofid2  6327  caofcom  6328  frxp  6448  fnse  6455  brovex  6466  riotasv3d  6590  tfr3  6652  tz7.48-2  6691  oaf1o  6798  omlimcl  6813  oeeulem  6836  ixpexg  7078  f1domg  7119  domdifsn  7183  unxpdom2  7309  xpfir  7323  fofinf1o  7379  fofi  7384  imafi  7391  intrnfi  7413  ordtypelem6  7484  oiexg  7496  cantnfp1lem3  7628  cantnflem1  7637  infxpenlem  7887  fseqenlem2  7898  ssnum  7912  acni2  7919  finacn  7923  fonum  7931  infpwfien  7935  inffien  7936  infunsdom1  8085  infunsdom  8086  ackbij1lem12  8103  cfslb2n  8140  fin23lem28  8212  compssiso  8246  isf34lem5  8250  fin56  8265  axcc3  8310  axdc3lem2  8323  ttukeylem6  8386  ttukeylem7  8387  brdom3  8398  gchdomtri  8496  fpwwe2lem13  8509  gchxpidm  8536  tsken  8621  tsksn  8627  tsk1  8631  tsk2  8632  2domtsk  8633  tskcard  8648  r1tskina  8649  gruss  8663  gruxp  8674  gruina  8685  grur1a  8686  ltaddpr  8903  ltexprlem7  8911  1idsr  8965  addgt0sr  8971  recexsr  8974  msqgt0  9540  mulgt1  9861  gt0div  9868  ge0div  9869  ltdiv2  9887  ltrec1  9889  lerec2  9890  lediv2  9892  lediv12a  9895  recreclt  9901  creur  9986  nn2ge  10017  avgle1  10199  recnz  10337  suprzcl  10341  uzwo2  10533  rpnnen1lem5  10596  xrrege0  10754  xlemul1a  10859  xrsupsslem  10877  xrinfmsslem  10878  supxr2  10884  supxrpnf  10889  supxrunb1  10890  supxrunb2  10891  ixxun  10924  peano2fzor  11186  ioopnfsup  11237  modcl  11245  modge0  11249  zmodcl  11258  seqcl  11335  seqf  11336  seqfveq  11339  sermono  11347  seqsplit  11348  seqcaopr2  11351  seqf1olem2  11355  seqf1o  11356  seqhomo  11362  seqz  11363  le2sq2  11449  faclbnd4lem3  11578  bcpasc  11604  hashgt0  11654  seqcoll  11704  seqcoll2  11705  ccatlid  11740  ccatass  11742  ccatswrd  11765  wrdeqcats1  11780  wrdeqs1cat  11781  revccat  11790  revrev  11791  sqrlem7  12046  resqrex  12048  sqrgt0  12056  leabs  12096  absmax  12125  r19.2uz  12147  lo1bdd2  12310  o1lo12  12324  rlimclim1  12331  lo1eq  12354  rlimeq  12355  rlimcn1  12374  rlimcn2  12376  rlimdiv  12431  rlimsqzlem  12434  clim2ser  12440  clim2ser2  12441  climub  12447  isercolllem1  12450  isercolllem3  12452  isercoll2  12454  climsup  12455  serf0  12466  iseraltlem1  12467  fsumf1o  12509  fsumss  12511  fsumsplit  12525  fsum2dlem  12546  fsumless  12567  fsumabs  12572  fsumtscopo  12573  fsumparts  12577  fsumrlim  12582  fsumo1  12583  o1fsum  12584  cvgcmp  12587  cvgcmpce  12589  fsumiun  12592  binom1dif  12604  incexclem  12608  incexc  12609  isumsplit  12612  isumrpcl  12615  isumless  12617  isumsup2  12618  isumltss  12620  climcnds  12623  supcvg  12627  expcnv  12635  explecnv  12636  geomulcvg  12645  cvgrat  12652  mertenslem1  12653  efcllem  12672  ef0lem  12673  eftlub  12702  tanval3  12727  tanneg  12741  rpnnen2lem7  12812  rpnnen2lem9  12814  rpnnen2lem11  12816  ruclem9  12829  dvdssubr  12883  divalgmod  12918  bitsf1  12950  algfx  13063  eucalgcvga  13069  isprm6  13101  phimullem  13160  eulerthlem2  13163  pcid  13238  pcgcd  13243  unbenlem  13268  prmreclem4  13279  prmreclem5  13280  4sqlem9  13306  4sqlem15  13319  4sqlem16  13320  vdwlem2  13342  vdwlem6  13346  vdwlem10  13350  vdwlem11  13351  vdwlem13  13353  ramval  13368  ressabs  13519  imasaddflem  13747  imasvscaf  13756  mrcid  13830  mrcidb  13832  mrcidm  13836  fucidcl  14154  setcmon  14234  setcepi  14235  catccatid  14249  xpccatid  14277  yonedalem4c  14366  yonedainv  14370  pospo  14422  latjlej1  14486  latmlem1  14502  latledi  14510  latj32  14518  latjjdi  14524  mrelatlub  14604  mreclat  14605  psss  14638  tsrlemax  14644  spwpr4c  14656  grpidd  14710  ismndd  14711  issubmnd  14716  subsubm  14749  gsumress  14769  gsumval2  14775  grpinvid1  14845  grpinvid2  14846  grplcan  14849  grpinvinv  14850  grpinvval2  14864  mulgass  14912  mulgpropd  14915  subginv  14943  subgmulg  14950  issubg2  14951  issubg4  14953  subsubg  14955  eqger  14982  divsinv  14991  resghm  15014  pwsdiagghm  15025  conjsubgen  15030  conjnsg  15033  subgga  15069  gass  15070  gasubg  15071  orbstafun  15080  orbsta  15082  gexcl2  15215  gexdvds3  15216  sylow1lem2  15225  sylow2blem1  15246  pj1ghm  15327  frgpup1  15399  frgpup3lem  15401  cntzspan  15452  cyggeninv  15485  lt6abl  15496  cycsubgcyg  15502  gsumval3eu  15505  gsumval3  15506  gsumzres  15509  gsumzaddlem  15518  gsumzsplit  15521  gsum2d  15538  gsum2d2lem  15539  dprdres  15578  dprdz  15580  dmdprdsplitlem  15587  dprdcntz2  15588  dprddisj2  15589  dprd2dlem1  15591  dmdprdsplit2lem  15595  dmdprdsplit2  15596  dprdsplit  15598  ablfac1c  15621  ablfac1eulem  15622  ablfac1eu  15623  pgpfac1lem2  15625  ablfac2  15639  rngidss  15682  isrngd  15690  rnglz  15692  rngrz  15693  gsumdixp  15707  0unit  15777  unitnegcl  15778  rnginvdv  15791  invrpropd  15795  subrg1  15870  subrginv  15876  issubrg2  15880  subsubrg  15886  abvneg  15914  lmod0vs  15975  lmodvs0  15976  lmodvneg1  15979  islss3  16027  lspsnsubg  16048  lspidm  16054  lspsnneg  16074  lmhmlsp  16117  drngnidl  16292  psrass1lem  16434  psrlinv  16453  psrlidm  16459  mplsubglem  16490  mplcoe1  16520  mplcoe2  16522  mplind  16554  xrsdsreval  16735  xrsdsreclb  16737  mulgrhm  16779  znfld  16833  cygznlem3  16842  ocvlsp  16895  pjff  16931  pjf2  16933  pjfo  16934  ocvpj  16936  ishil2  16938  tgcl  17026  tgclb  17027  tgss2  17044  tgfiss  17048  opncld  17089  ntrval2  17107  ntrss3  17116  clsidm  17123  ntridm  17124  opnssneib  17171  ssnei2  17172  neindisj  17173  opnnei  17176  innei  17181  resttopon  17217  restcld  17228  restcls  17237  restntr  17238  perfopn  17241  cnpnei  17320  cncls2i  17326  cnntri  17327  cnclsi  17328  lmss  17354  pnrmopn  17399  lpcls  17420  perfcls  17421  cncmp  17447  cmpsublem  17454  cmpsub  17455  consuba  17475  clscon  17485  1stcrest  17508  lly1stc  17551  hauspwdom  17556  llycmpkgen2  17574  ptclsg  17639  txcnp  17644  txcmplem1  17665  xkococnlem  17683  qtoptopon  17728  qtopid  17729  kqopn  17758  ptunhmeo  17832  trfbas2  17867  trfbas  17868  filin  17878  filintn0  17885  trfil2  17911  fgtr  17914  trufil  17934  cfinufil  17952  elfm3  17974  fmfnfmlem4  17981  neiflim  17998  flfval  18014  flfnei  18015  fclsbas  18045  ptcmplem5  18079  cnextf  18089  cnextfres  18091  tgplacthmeo  18125  tgpconcompeqg  18133  tgpconcomp  18134  tsmssubm  18164  tsmssplit  18173  tsmsxplem1  18174  restutopopn  18260  isucn2  18301  cnextucn  18325  blpnfctr  18458  mopni2  18515  stdbdmopn  18540  met1stc  18543  metutopOLD  18604  psmetutop  18605  nrmmetd  18614  tngngp2  18685  xrsxmet  18832  metdsle  18874  climcncf  18922  icoopnst  18956  iocopnst  18957  cnheibor  18972  bndth  18975  htpyco1  18995  htpyco2  18996  phtpyco2  19007  pi1xfr  19072  pi1coghm  19078  lmmbrf  19207  lmnn  19208  caucfil  19228  cmetcaulem  19233  iscmet3  19238  cfilresi  19240  caussi  19242  causs  19243  lmle  19246  lmclimf  19248  bcthlem4  19272  bcth3  19276  minveclem4  19325  ivth2  19344  ivthicc  19347  cniccbdd  19350  ovollb2  19377  ovolctb  19378  ovolunlem1a  19384  ovolunlem1  19385  ovolshftlem1  19397  ovolicc2lem1  19405  ovolicc2lem2  19406  ovolicc2lem4  19408  ovolicc2lem5  19409  uniioombllem2  19467  uniioombllem3  19469  volivth  19491  mbfss  19530  mbflimsup  19550  itg1val2  19568  i1fadd  19579  i1fmul  19580  itg1addlem4  19583  i1fmulc  19587  itg1mulc  19588  mbfi1fseqlem4  19602  itg2const2  19625  itg2seq  19626  itg2splitlem  19632  itg2split  19633  itg2addlem  19642  itg2gt0  19644  itg2cnlem2  19646  iblss  19688  iblss2  19689  itgss3  19698  itgless  19700  itgfsum  19710  itgsplit  19719  itgsplitioo  19721  itgcn  19726  ditgcl  19737  ditgswap  19738  ditgsplitlem  19739  dvconst  19795  dvaddbr  19816  dvmulbr  19817  rolle  19866  dvlip  19869  dvlipcn  19870  dvlip2  19871  dveq0  19876  dv11cn  19877  dvivthlem1  19884  dvne0  19887  lhop1lem  19889  lhop2  19891  lhop  19892  dvcnvre  19895  dvfsumle  19897  dvfsumge  19898  dvfsumabs  19899  dvfsumlem2  19903  dvfsumlem3  19904  dvfsumrlimge0  19906  dvfsumrlim  19907  ftc1lem1  19911  ftc1lem4  19915  ftc1lem5  19916  itgsubstlem  19924  evl1sca  19942  mpfind  19957  deg1sclle  20027  uc1pmon1p  20066  plymullem  20127  coeeulem  20135  dgrlem  20140  dgrlb  20147  coemulhi  20164  dgrcolem2  20184  plydiveu  20207  vieta1lem2  20220  vieta1  20221  taylplem1  20271  taylplem2  20272  dvtaylp  20278  taylthlem1  20281  taylthlem2  20282  ulmdvlem1  20308  mtest  20312  radcnv0  20324  pserulm  20330  pserdvlem2  20336  abelthlem3  20341  abelthlem5  20343  abelthlem7  20346  efcvx  20357  sineq0  20421  tanord  20432  tanregt0  20433  logne0  20489  argregt0  20497  argimgt0  20499  argimlt0  20500  logneg2  20502  logcnlem3  20527  cxpsqr  20586  loglesqr  20634  ang180lem2  20644  isosctrlem1  20654  dcubic  20678  atanlogaddlem  20745  atanlogsub  20748  atantan  20755  atans2  20763  log2tlbnd  20777  birthdaylem2  20783  rlimcnp  20796  efrlim  20800  jensenlem1  20817  jensenlem2  20818  jensen  20819  fsumharmonic  20842  wilthlem2  20844  ftalem4  20850  ftalem5  20851  basellem3  20857  basellem4  20858  ppisval  20878  chtdif  20933  dvdsflsumcom  20965  musumsum  20969  muinv  20970  sgmmul  20977  chtleppi  20986  chtublem  20987  fsumvma  20989  chpval2  20994  chpub  20996  bposlem3  21062  lgsvalmod  21091  lgsdir2  21104  lgsdchr  21124  lgsquadlem2  21131  lgsquad2lem2  21135  chebbnd1lem1  21155  chebbnd1lem3  21157  dchrisumlem1  21175  dchrisumlem2  21176  dchrisumlem3  21177  dchrisum0fno1  21197  rpvmasum2  21198  dchrisum0lem1b  21201  dchrisum0lem1  21202  mulog2sumlem2  21221  chpdifbndlem1  21239  pntrsumbnd2  21253  pntrlog2bndlem6  21269  pntpbnd1  21272  pntlemj  21289  pntlemf  21291  qabvle  21311  padicabv  21316  padicabvcxp  21318  ostth2lem3  21321  usgraedg3  21397  usgrarnedg1  21400  fargshiftfo  21617  grpoidinvlem2  21785  grpoidinvlem3  21786  grpoideu  21789  grpoinvid1  21810  grpoinvid2  21811  grpolcan  21813  grpo2inv  21819  grpoinvop  21821  grpomuldivass  21829  grpopnpcan2  21833  grponnncan2  21834  grponpncan  21835  gxinv  21850  gxid  21853  ablo4  21867  ablomuldiv  21869  ablodivdiv4  21871  ablonnncan  21873  ablonnncan1  21875  ghgrplem1  21946  ghgrp  21948  ghablo  21949  ghsubgolem  21950  rngolz  21981  rngorz  21982  vc0  22040  vcz  22041  nvzs  22118  nvmdi  22123  nvnegneg  22124  nvsubadd  22128  nvnpcan  22133  nvmeq0  22137  nvabs  22154  nvelbl2  22178  sspmval  22224  sspz  22226  sspival  22229  sspimsval  22231  nmoub3i  22266  nmblolbii  22292  dipsubdir  22341  sspph  22348  ubthlem1  22364  minvecolem3  22370  minvecolem4  22374  htthlem  22412  hvaddsub4  22572  hi2eq  22599  shsel3  22809  pjpreeq  22892  pjeq  22893  chabs1  23010  pjspansn  23071  chscllem1  23131  chscllem2  23132  chscllem4  23134  5oalem2  23149  3oalem2  23157  pjoi0  23211  nmopub2tALT  23404  nmfnleub2  23421  eigvalcl  23456  eighmre  23458  leopmul  23629  nmopleid  23634  opsqrlem4  23638  spansncv2  23788  chcv1  23850  atcv0eq  23874  atexch  23876  chirredi  23889  cdj1i  23928  elabreximd  23983  abfmpeld  24058  iocinif  24136  ressmulgnn  24197  dvrdir  24218  rhmunitinv  24252  kerunit  24253  zzsmulg  24257  remulg  24262  metider  24281  tpr2rico  24302  lmdvg  24330  rezh  24347  qqhvq  24363  logbrec  24397  indsum  24412  indpreima  24414  indf1ofs  24415  esummono  24442  esumpcvgval  24460  esumpmono  24461  esumcvg  24468  sigaclfu2  24496  cldssbrsiga  24533  probun  24669  ballotlemfc0  24742  ballotlemfcc  24743  ballotlemsel1i  24762  ballotlemsima  24765  ballotlemfrceq  24778  ballotlemirc  24781  dmlogdmgm  24800  subfacp1lem4  24861  subfacp1lem5  24862  erdszelem8  24876  ptpcon  24912  cvmliftmolem1  24960  cvmliftmolem2  24961  cvmliftlem6  24969  cvmliftlem7  24970  cvmliftlem10  24973  cvmlift2lem9  24990  cvmlift2lem11  24992  cvmlift2lem12  24993  ghomgsg  25096  ghomf1olem  25097  sinccvglem  25101  lediv2aALT  25109  rtrclreclem.trans  25138  clim2prod  25208  clim2div  25209  ntrivcvgfvn0  25219  ntrivcvgmullem  25221  fprodf1o  25264  prodss  25265  fprodss  25266  fprodser  25267  fprodsplit  25281  fprodeq0  25291  fprod2dlem  25296  binomfallfaclem2  25348  dfon2lem9  25410  sltval2  25603  colinearalg  25841  axcontlem2  25896  axcontlem7  25901  outsideofeq  26056  lineelsb2  26074  bpolysum  26091  bpolydiflem  26092  onsuct0  26183  mblfinlem  26234  voliunnfl  26240  volsupnfl  26241  itg2gt0cn  26250  itgaddnclem2  26254  bddiblnc  26265  ftc1cnnclem  26268  ftc1cnnc  26269  ftc1anclem2  26271  ftc1anclem5  26274  ftc1anclem6  26275  ftc1anclem7  26276  ftc1anclem8  26277  ftc1anc  26278  ftc2nc  26279  areacirc  26288  opnregcld  26324  isfne  26339  lfinpfin  26374  sdclem1  26438  fdc  26440  metf1o  26452  mettrifi  26454  equivtotbnd  26478  isbnd2  26483  bndss  26486  equivbnd2  26492  ismtyima  26503  ismtybndlem  26506  heiborlem1  26511  heiborlem8  26518  ismrer1  26538  ablo4pnp  26546  ghomdiv  26550  rngoneglmul  26558  rngonegrmul  26559  rngosubdi  26560  rngosubdir  26561  isdrngo2  26565  rngohomco  26581  rngoisoco  26589  iscringd  26600  crngm4  26604  idlsubcl  26624  divrngidl  26629  unichnidl  26632  keridl  26633  maxidln1  26645  maxidln0  26646  igenidl  26664  igenidl2  26666  ispridlc  26671  dmncan1  26677  elrfirn2  26741  2rexfrabdioph  26847  3rexfrabdioph  26848  4rexfrabdioph  26849  6rexfrabdioph  26850  7rexfrabdioph  26851  elnn0rabdioph  26854  irrapxlem5  26880  pell14qrre  26911  pell14qrne0  26912  pell14qrmulcl  26917  pellfundex  26940  monotoddzzfi  26996  jm2.17c  27018  fnwe2lem2  27117  frlmsslsp  27216  islinds2  27251  f1lindf  27260  flcidc  27347  psgnunilem5  27385  expgrowthi  27518  rfcnpre1  27657  rfcnpre2  27669  fmulcl  27678  fmul01lt1lem1  27681  fmul01lt1lem2  27682  climinf  27699  stoweidlem11  27727  stoweidlem14  27730  stoweidlem20  27736  stoweidlem26  27742  stoweidlem27  27743  stoweidlem31  27747  stoweidlem48  27764  stoweidlem51  27767  swrdccatin2  28176  2cshwmod  28223  onetansqsecsq  28441  bnj594  29220  lssats  29747  lfl0  29800  lfladdcl  29806  lflvscl  29812  lkr0f  29829  olm11  29962  latm12  29965  cvrle  30013  cvrnle  30015  cvrne  30016  cvrval3  30147  atcvrj0  30162  atltcvr  30169  atbtwnexOLDN  30181  atbtwnex  30182  3at  30224  2atneat  30249  llncvrlpln2  30291  lplncvrlvol2  30349  dalemdnee  30400  linepsubN  30486  isline2  30508  paddasslem17  30570  pmodN  30584  pmapjlln1  30589  pclidN  30630  polval2N  30640  polssatN  30642  polpmapN  30646  2polpmapN  30647  2polvalN  30648  2polssN  30649  3polN  30650  pclss2polN  30655  2pmaplubN  30660  polatN  30665  2polatN  30666  psubclsubN  30674  pmapidclN  30676  ispsubcl2N  30681  linepsubclN  30685  polsubclN  30686  lhpoc2N  30749  ltrnlaut  30857  ltrncnv  30880  cdlemc3  30927  cdleme3b  30963  cdleme42ke  31219  trlcoat  31457  tendoid  31507  tendoex  31709  dvalveclem  31760  diaintclN  31793  diasslssN  31794  dvhgrp  31842  dvhlveclem  31843  docaclN  31859  diaocN  31860  doca2N  31861  doca3N  31862  dvadiaN  31863  djaclN  31871  djajN  31872  dibval2  31879  dibvalrel  31898  dibintclN  31902  dicvalrelN  31920  xihopellsmN  31989  dihopellsm  31990  dihsslss  32011  dih1  32021  dih1dimatlem  32064  dihlspsnat  32068  dihintcl  32079  dihmeetcl  32080  dochval2  32087  dochcl  32088  dochlss  32089  dochssv  32090  dochvalr  32092  dochvalr2  32097  dochocss  32101  dochoc  32102  dochnoncon  32126  djhcl  32135  djhlj  32136  djhexmid  32146  dvh3dim3N  32184  lcfrlem21  32298  hlhilhillem  32698
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