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

Theorem syldan 456
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 424 . . 3  |-  ( ch 
->  ( ph  ->  th )
)
43adantrd 454 . 2  |-  ( ch 
->  ( ( ph  /\  ps )  ->  th )
)
51, 4mpcom 32 1  |-  ( (
ph  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  sylan2  460  sbcied2  3030  csbied2  3126  elpw2g  4176  pofun  4332  elpwunsn  4570  fnbr  5348  dffv2  5594  fnexALT  5744  grprinvlem  6060  caofid0l  6107  caofid0r  6108  caofid1  6109  caofid2  6110  caofcom  6111  frxp  6227  fnse  6234  riotasv3d  6355  tfr3  6417  tz7.48-2  6456  oaf1o  6563  omlimcl  6578  oeeulem  6601  ixpexg  6842  f1domg  6883  domdifsn  6947  unxpdom2  7073  xpfir  7087  fofinf1o  7139  fofi  7144  imafi  7150  intrnfi  7172  ordtypelem6  7240  oiexg  7252  cantnfp1lem3  7384  cantnflem1  7393  infxpenlem  7643  fseqenlem2  7654  ssnum  7668  acni2  7675  finacn  7679  fonum  7687  infpwfien  7691  inffien  7692  infunsdom1  7841  infunsdom  7842  ackbij1lem12  7859  cfslb2n  7896  fin23lem28  7968  compssiso  8002  isf34lem5  8006  fin56  8021  axcc3  8066  axdc3lem2  8079  ttukeylem6  8143  ttukeylem7  8144  brdom3  8155  gchdomtri  8253  fpwwe2lem13  8266  gchxpidm  8293  tsken  8378  tsksn  8384  tsk1  8388  tsk2  8389  2domtsk  8390  tskcard  8405  r1tskina  8406  gruss  8420  gruxp  8431  gruina  8442  grur1a  8443  ltaddpr  8660  ltexprlem7  8668  1idsr  8722  addgt0sr  8728  recexsr  8731  msqgt0  9296  mulgt1  9617  gt0div  9624  ge0div  9625  ltdiv2  9643  ltrec1  9645  lerec2  9646  lediv2  9648  lediv12a  9651  recreclt  9657  creur  9742  nn2ge  9773  avgle1  9953  recnz  10089  suprzcl  10093  uzwo2  10285  rpnnen1lem5  10348  xrrege0  10505  xlemul1a  10610  xrsupsslem  10627  xrinfmsslem  10628  supxr2  10634  supxrpnf  10639  supxrunb1  10640  supxrunb2  10641  ixxun  10674  peano2fzor  10921  ioopnfsup  10970  modcl  10978  modge0  10982  zmodcl  10991  seqcl  11068  seqf  11069  seqfveq  11072  sermono  11080  seqsplit  11081  seqcaopr2  11084  seqf1olem2  11088  seqf1o  11089  seqhomo  11095  seqz  11096  le2sq2  11181  faclbnd4lem3  11310  bcpasc  11335  seqcoll  11403  seqcoll2  11404  ccatlid  11436  ccatass  11438  ccatswrd  11461  wrdeqcats1  11476  wrdeqs1cat  11477  revccat  11486  revrev  11487  sqrlem7  11736  resqrex  11738  sqrgt0  11746  leabs  11786  absmax  11815  r19.2uz  11837  lo1bdd2  12000  o1lo12  12014  rlimclim1  12021  lo1eq  12044  rlimeq  12045  rlimcn1  12064  rlimcn2  12066  rlimdiv  12121  rlimsqzlem  12124  clim2ser  12130  clim2ser2  12131  climub  12137  isercolllem1  12140  isercolllem3  12142  isercoll2  12144  climsup  12145  serf0  12155  iseraltlem1  12156  fsumf1o  12198  fsumss  12200  fsumsplit  12214  fsum2dlem  12235  fsumless  12256  fsumabs  12261  fsumtscopo  12262  fsumparts  12266  fsumrlim  12271  fsumo1  12272  o1fsum  12273  cvgcmp  12276  cvgcmpce  12278  fsumiun  12281  binom1dif  12293  incexclem  12297  incexc  12298  isumsplit  12301  isumrpcl  12304  isumless  12306  isumsup2  12307  isumltss  12309  climcnds  12312  supcvg  12316  expcnv  12324  explecnv  12325  geomulcvg  12334  cvgrat  12341  mertenslem1  12342  efcllem  12361  ef0lem  12362  eftlub  12391  tanval3  12416  tanneg  12430  rpnnen2lem7  12501  rpnnen2lem9  12503  rpnnen2lem11  12505  ruclem9  12518  dvdssubr  12572  divalgmod  12607  bitsf1  12639  algfx  12752  eucalgcvga  12758  isprm6  12790  phimullem  12849  eulerthlem2  12852  pcid  12927  pcgcd  12932  unbenlem  12957  prmreclem4  12968  prmreclem5  12969  4sqlem9  12995  4sqlem15  13008  4sqlem16  13009  vdwlem2  13031  vdwlem6  13035  vdwlem10  13039  vdwlem11  13040  vdwlem13  13042  ramval  13057  ressabs  13208  imasaddflem  13434  imasvscaf  13443  mrcid  13517  mrcidb  13519  mrcidm  13523  fucidcl  13841  setcmon  13921  setcepi  13922  catccatid  13936  xpccatid  13964  yonedalem4c  14053  yonedainv  14057  pospo  14109  latjlej1  14173  latmlem1  14189  latledi  14197  latj32  14205  latjjdi  14211  ipoval  14259  mrelatlub  14291  mreclat  14292  psss  14325  tsrlemax  14331  spwpr4c  14343  grpidd  14397  ismndd  14398  issubmnd  14403  subsubm  14436  gsumress  14456  gsumval2  14462  grpinvid1  14532  grpinvid2  14533  grplcan  14536  grpinvinv  14537  grpinvval2  14551  mulgass  14599  mulgpropd  14602  subginv  14630  subgmulg  14637  issubg2  14638  issubg4  14640  subsubg  14642  eqger  14669  divsinv  14678  resghm  14701  pwsdiagghm  14712  conjsubgen  14717  conjnsg  14720  subgga  14756  gass  14757  gasubg  14758  orbstafun  14767  orbsta  14769  gexcl2  14902  gexdvds3  14903  sylow1lem2  14912  sylow2blem1  14933  pj1ghm  15014  frgpup1  15086  frgpup3lem  15088  cntzspan  15139  cyggeninv  15172  lt6abl  15183  cycsubgcyg  15189  gsumval3eu  15192  gsumval3  15193  gsumzres  15196  gsumzaddlem  15205  gsumzsplit  15208  gsum2d  15225  gsum2d2lem  15226  dprdres  15265  dprdz  15267  dmdprdsplitlem  15274  dprdcntz2  15275  dprddisj2  15276  dprd2dlem1  15278  dmdprdsplit2lem  15282  dmdprdsplit2  15283  dprdsplit  15285  ablfac1c  15308  ablfac1eulem  15309  ablfac1eu  15310  pgpfac1lem2  15312  ablfac2  15326  rngidss  15369  isrngd  15377  rnglz  15379  rngrz  15380  gsumdixp  15394  0unit  15464  unitnegcl  15465  rnginvdv  15478  invrpropd  15482  subrg1  15557  subrginv  15563  issubrg2  15567  subsubrg  15573  abvneg  15601  lmod0vs  15665  lmodvs0  15666  lmodvneg1  15669  islss3  15718  lspsnsubg  15739  lspidm  15745  lspsnneg  15765  lmhmlsp  15808  drngnidl  15983  psrass1lem  16125  psrlinv  16144  psrlidm  16150  mplsubglem  16181  mplcoe1  16211  mplcoe2  16213  mplind  16245  xrsdsreval  16418  xrsdsreclb  16420  mulgrhm  16462  znfld  16516  cygznlem3  16525  ocvlsp  16578  pjff  16614  pjf2  16616  pjfo  16617  ocvpj  16619  ishil2  16621  tgcl  16709  tgclb  16710  tgss2  16727  tgfiss  16731  opncld  16772  ntrval2  16790  ntrss3  16799  clsidm  16806  ntridm  16807  opnssneib  16854  ssnei2  16855  neindisj  16856  opnnei  16859  innei  16864  resttopon  16894  restcld  16905  restcls  16913  restntr  16914  perfopn  16917  cnpnei  16995  cncls2i  17001  cnntri  17002  cnclsi  17003  lmss  17028  pnrmopn  17073  lpcls  17094  perfcls  17095  cncmp  17121  cmpsublem  17128  cmpsub  17129  consuba  17148  clscon  17158  1stcrest  17181  lly1stc  17224  hauspwdom  17229  llycmpkgen2  17247  ptclsg  17311  txcnp  17316  txcmplem1  17337  xkococnlem  17355  qtoptopon  17397  qtopid  17398  kqopn  17427  ptunhmeo  17501  trfbas2  17540  trfbas  17541  filin  17551  filintn0  17558  trfil2  17584  fgtr  17587  trufil  17607  cfinufil  17625  elfm3  17647  fmfnfmlem4  17654  neiflim  17671  flfval  17687  flfnei  17688  fclsbas  17718  ptcmplem5  17752  tgplacthmeo  17788  tgpconcompeqg  17796  tgpconcomp  17797  tsmssubm  17827  tsmssplit  17836  tsmsxplem1  17837  blpnfctr  17984  mopni2  18041  stdbdmopn  18066  met1stc  18069  nrmmetd  18099  tngngp2  18170  xrsxmet  18317  metdsle  18358  climcncf  18406  icoopnst  18439  iocopnst  18440  cnheibor  18455  bndth  18458  htpyco1  18478  htpyco2  18479  phtpyco2  18490  pi1xfr  18555  pi1coghm  18561  lmmbrf  18690  lmnn  18691  caucfil  18711  cmetcaulem  18716  iscmet3  18721  cfilresi  18723  caussi  18725  causs  18726  lmle  18729  lmclimf  18731  bcthlem4  18751  bcth3  18755  minveclem4  18798  ivth2  18817  ivthicc  18820  cniccbdd  18823  ovollb2  18850  ovolctb  18851  ovolunlem1a  18857  ovolunlem1  18858  ovolshftlem1  18870  ovolicc2lem1  18878  ovolicc2lem2  18879  ovolicc2lem4  18881  ovolicc2lem5  18882  uniioombllem2  18940  uniioombllem3  18942  volivth  18964  mbfss  19003  mbflimsup  19023  itg1val2  19041  i1fadd  19052  i1fmul  19053  itg1addlem4  19056  i1fmulc  19060  itg1mulc  19061  mbfi1fseqlem4  19075  itg2const2  19098  itg2seq  19099  itg2splitlem  19105  itg2split  19106  itg2addlem  19115  itg2gt0  19117  itg2cnlem2  19119  iblss  19161  iblss2  19162  itgss3  19171  itgless  19173  itgfsum  19183  itgsplit  19192  itgsplitioo  19194  itgcn  19199  ditgcl  19210  ditgswap  19211  ditgsplitlem  19212  dvconst  19268  dvaddbr  19289  dvmulbr  19290  dvcnvlem  19325  rolle  19339  dvlip  19342  dvlipcn  19343  dvlip2  19344  dveq0  19349  dv11cn  19350  dvivthlem1  19357  dvne0  19360  lhop1lem  19362  lhop2  19364  lhop  19365  dvcnvre  19368  dvfsumle  19370  dvfsumge  19371  dvfsumabs  19372  dvfsumlem2  19376  dvfsumlem3  19377  dvfsumrlimge0  19379  dvfsumrlim  19380  ftc1lem1  19384  ftc1lem4  19388  ftc1lem5  19389  itgsubstlem  19397  evl1sca  19415  mpfind  19430  deg1sclle  19500  plymullem  19600  coeeulem  19608  dgrlem  19613  dgrlb  19620  coemulhi  19637  dgrcolem2  19657  plydiveu  19680  vieta1lem2  19693  vieta1  19694  taylplem1  19744  taylplem2  19745  dvtaylp  19751  taylthlem1  19754  taylthlem2  19755  ulmdvlem1  19779  mtest  19783  radcnv0  19794  pserulm  19800  pserdvlem2  19806  abelthlem3  19811  abelthlem5  19813  abelthlem7  19816  efcvx  19827  sineq0  19891  tanord  19902  tanregt0  19903  logne0  19958  argregt0  19966  argimgt0  19968  argimlt0  19969  logneg2  19971  logcnlem3  19993  cxpsqr  20052  loglesqr  20100  ang180lem2  20110  isosctrlem1  20120  dcubic  20144  atanlogaddlem  20211  atanlogsub  20214  atantan  20221  atans2  20229  log2tlbnd  20243  birthdaylem2  20249  rlimcnp  20262  efrlim  20266  jensenlem1  20283  jensenlem2  20284  jensen  20285  fsumharmonic  20307  wilthlem2  20309  ftalem4  20315  ftalem5  20316  basellem3  20322  basellem4  20323  ppisval  20343  chtdif  20398  dvdsflsumcom  20430  musumsum  20434  muinv  20435  sgmmul  20442  chtleppi  20451  chtublem  20452  fsumvma  20454  chpval2  20459  chpub  20461  bposlem3  20527  lgsvalmod  20556  lgsdir2  20569  lgsdchr  20589  lgsquadlem2  20596  lgsquad2lem2  20600  chebbnd1lem1  20620  chebbnd1lem3  20622  dchrisumlem1  20640  dchrisumlem2  20641  dchrisumlem3  20642  dchrisum0fno1  20662  rpvmasum2  20663  dchrisum0lem1b  20666  dchrisum0lem1  20667  mulog2sumlem2  20686  chpdifbndlem1  20704  pntrsumbnd2  20718  pntrlog2bndlem6  20734  pntpbnd1  20737  pntlemj  20754  pntlemf  20756  qabvle  20776  padicabv  20781  padicabvcxp  20783  ostth2lem3  20786  grpoidinvlem2  20874  grpoidinvlem3  20875  grpoideu  20878  grpoinvid1  20899  grpoinvid2  20900  grpolcan  20902  grpo2inv  20908  grpoinvop  20910  grpomuldivass  20918  grpopnpcan2  20922  grponnncan2  20923  grponpncan  20924  gxinv  20939  gxid  20942  ablo4  20956  ablomuldiv  20958  ablodivdiv4  20960  ablonnncan  20962  ablonnncan1  20964  ghgrplem1  21035  ghgrp  21037  ghablo  21038  ghsubgolem  21039  rngolz  21070  rngorz  21071  vc0  21127  vcz  21128  nvzs  21205  nvmdi  21210  nvnegneg  21211  nvsubadd  21215  nvnpcan  21220  nvmeq0  21224  nvabs  21241  nvelbl2  21265  sspmval  21311  sspz  21313  sspival  21316  sspimsval  21318  nmoub3i  21353  nmblolbii  21379  dipsubdir  21428  sspph  21435  ubthlem1  21451  minvecolem3  21457  minvecolem4  21461  htthlem  21499  hvaddsub4  21659  hi2eq  21686  shsel3  21896  pjpreeq  21979  pjeq  21980  chabs1  22097  pjspansn  22158  chscllem1  22218  chscllem2  22219  chscllem4  22221  5oalem2  22236  3oalem2  22244  pjoi0  22298  nmopub2tALT  22491  nmfnleub2  22508  eigvalcl  22543  eighmre  22545  leopmul  22716  nmopleid  22721  opsqrlem4  22725  spansncv2  22875  chcv1  22937  atcv0eq  22961  atexch  22963  chirredi  22976  cdj1i  23015  elabreximd  23041  ballotlemfp1  23052  ballotlemimin  23066  ballotlemsel1i  23073  ballotlemsima  23076  ballotlemfrceq  23089  ballotlemirc  23092  iocinif  23276  tpr2rico  23298  ressmulgnn  23310  lmdvg  23378  hashgt0  23389  logbrec  23409  esumpcvgval  23448  esumpmono  23449  esumcvg  23456  sigaclfu2  23484  cldssbrsiga  23520  indsum  23608  subfacp1lem4  23716  subfacp1lem5  23717  erdszelem8  23731  ptpcon  23766  cvmliftmolem1  23814  cvmliftmolem2  23815  cvmliftlem6  23823  cvmliftlem7  23824  cvmliftlem10  23827  cvmlift2lem9  23844  cvmlift2lem11  23846  cvmlift2lem12  23847  ghomgsg  24002  ghomf1olem  24003  sinccvglem  24007  lediv2aALT  24015  rtrclreclem.trans  24045  dfon2lem9  24149  sltval2  24312  colinearalg  24540  axcontlem2  24595  axcontlem7  24600  outsideofeq  24755  lineelsb2  24773  bpolysum  24790  bpolydiflem  24791  onsuct0  24882  areacirc  24942  fprod1fi  25337  grpodrcan  25386  ltrinvlem  25417  invaddvec  25478  dblsubvec  25485  mvecrtol2  25488  basexre  25533  intopcoaconb  25551  qusp  25553  cntrset  25613  msr4  25617  lvsovso  25637  lvsovso3  25639  dmrngcmp  25762  dualcat2  25795  idfisf  25852  prismorcsetlem  25923  isgraphmrph  25934  idmor  25957  domidmor  25959  codidmor  25961  grphidmor  25963  grphidmor3  25965  cmp2morpcats  25972  cmpidmor2  25980  cmpidmor3  25981  lemindclsbu  26006  isconc2  26018  opnregcld  26259  isfne  26279  lfinpfin  26314  sdclem1  26464  fdc  26466  metf1o  26480  mettrifi  26484  equivtotbnd  26513  isbnd2  26518  bndss  26521  equivbnd2  26527  ismtyima  26538  ismtybndlem  26541  heiborlem1  26546  heiborlem8  26553  ismrer1  26573  ablo4pnp  26581  ghomdiv  26585  rngoneglmul  26593  rngonegrmul  26594  rngosubdi  26595  rngosubdir  26596  isdrngo2  26600  rngohomco  26616  rngoisoco  26624  iscringd  26635  crngm4  26639  idlsubcl  26659  divrngidl  26664  unichnidl  26667  keridl  26668  maxidln1  26680  maxidln0  26681  igenidl  26699  igenidl2  26701  ispridlc  26706  dmncan1  26712  elrfirn2  26782  2rexfrabdioph  26888  3rexfrabdioph  26889  4rexfrabdioph  26890  6rexfrabdioph  26891  7rexfrabdioph  26892  elnn0rabdioph  26895  irrapxlem5  26922  pell14qrre  26953  pell14qrne0  26954  pell14qrmulcl  26959  pellfundex  26982  monotoddzzfi  27038  jm2.17c  27060  fnwe2lem2  27159  frlmsslsp  27259  islinds2  27294  f1lindf  27303  flcidc  27390  psgnunilem5  27428  expgrowthi  27561  sumpair  27717  climinf  27743  stoweidlem26  27786  stoweidlem27  27787  stoweidlem61  27821  onetansqsecsq  28242  bnj594  29017  lssats  29275  lfl0  29328  lfladdcl  29334  lflvscl  29340  lkr0f  29357  olm11  29490  latm12  29493  cvrle  29541  cvrnle  29543  cvrne  29544  cvrval3  29675  atcvrj0  29690  atltcvr  29697  atbtwnexOLDN  29709  atbtwnex  29710  3at  29752  2atneat  29777  llncvrlpln2  29819  lplncvrlvol2  29877  dalemdnee  29928  linepsubN  30014  isline2  30036  paddasslem17  30098  pmodN  30112  pmapjlln1  30117  pclidN  30158  polval2N  30168  polssatN  30170  polpmapN  30174  2polpmapN  30175  2polvalN  30176  2polssN  30177  3polN  30178  pclss2polN  30183  2pmaplubN  30188  polatN  30193  2polatN  30194  psubclsubN  30202  pmapidclN  30204  ispsubcl2N  30209  linepsubclN  30213  polsubclN  30214  lhpoc2N  30277  ltrnlaut  30385  ltrncnv  30408  cdlemc3  30455  cdleme3b  30491  cdleme42ke  30747  trlcoat  30985  tendoid  31035  tendoex  31237  dvalveclem  31288  diaintclN  31321  diasslssN  31322  dvhgrp  31370  dvhlveclem  31371  docaclN  31387  diaocN  31388  doca2N  31389  doca3N  31390  dvadiaN  31391  djaclN  31399  djajN  31400  dibval2  31407  dibvalrel  31426  dibintclN  31430  dicvalrelN  31448  xihopellsmN  31517  dihopellsm  31518  dihsslss  31539  dih1  31549  dih1dimatlem  31592  dihlspsnat  31596  dihintcl  31607  dihmeetcl  31608  dochval2  31615  dochcl  31616  dochlss  31617  dochssv  31618  dochvalr  31620  dochvalr2  31625  dochocss  31629  dochoc  31630  dochnoncon  31654  djhcl  31663  djhlj  31664  djhexmid  31674  dvh3dim3N  31712  lcfrlem21  31826  hlhilhillem  32226
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 177  df-an 360
  Copyright terms: Public domain W3C validator