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

Theorem syl6 33
Description: A syllogism rule of inference. The second premise is used to replace the consequent of the first premise. (Contributed by NM, 5-Jan-1993.) (Proof shortened by Wolf Lammen, 30-Jul-2012.)
Hypotheses
Ref Expression
syl6.1
syl6.2
Assertion
Ref Expression
syl6

Proof of Theorem syl6
StepHypRef Expression
1 syl6.1 . 2
2 syl6.2 . . 3
32a1i 11 . 2
41, 3sylcom 29 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  syl56  34  syl6com  35  a1dd  46  syl6mpi  62  syl6c  64  syl10  73  com34  83  con1d  124  expi  149  looinv  182  syl6ib  226  syl6ibr  227  syl6bi  228  syl6bir  229  jaoi  379  syl6an  545  a2andOLD  812  pm2.37  844  pm2.81  851  oplem1  964  3jao  1289  al2im  1635  exlimdv  1724  spimfw  1737  ax13b  1805  hbald  1848  19.9ht  1889  19.23t  1909  spimed  2007  cbv2h  2019  axc11n  2049  axc11nOLD  2050  ax12v2  2083  equvini  2087  hbsb2  2099  dfsb2  2114  sbequi  2116  sbft  2120  sbi1  2133  aev-o  2261  ax12eq  2271  ax12el  2272  ax12indn  2273  ax12indi  2274  mo3  2323  mo3OLD  2324  mopick  2356  moexex  2363  2eu1OLD  2377  dvelimdc  2642  necon1ad  2673  necon4bd  2679  rsp2  2831  rgen2aOLD  2885  mo2icl  3278  reu6  3288  reupick2  3783  elpwunsn  4070  pwpw0  4178  sssn  4188  pwsnALT  4244  dfiun2g  4362  disjiun  4442  axsep  4572  reusv3i  4659  reusv7OLD  4664  ralxfrALT  4671  opth1  4725  copsexg  4737  copsexgOLD  4738  opelopabt  4764  wefrc  4878  ordunidif  4931  oneqmini  4934  suctr  4966  ordsssuc2  4971  frinxp  5070  issref  5385  iotaval  5567  fv3  5884  ndmfv  5895  ssimaex  5938  fvopab3ig  5953  iinpreima  6017  fvcofneq  6039  dff3  6044  dff4  6045  ffnfv  6057  fnsnb  6090  fconstfvOLD  6134  elunirn  6163  f1mpt  6169  isomin  6233  oprabid  6323  mpt2eq123  6356  sorpsscmpl  6591  dfwe2  6617  ssorduni  6621  ssonprc  6627  nlimsucg  6677  ordunisuc2  6679  tfinds  6694  ssnlim  6718  fun11iun  6760  f1oweALT  6784  f1o2ndf1  6908  frxp  6910  soxp  6913  brtpos  6983  rntpos  6987  dftpos4  6993  onfununi  7031  onnseq  7034  smores2  7044  smo11  7054  tfr3  7087  rdglim2  7117  tz7.48lem  7125  tz7.49  7129  seqomlem2  7135  oawordex  7225  oa00  7227  oaass  7229  om00  7243  odi  7247  omass  7248  oeordi  7255  oelim2  7263  omsmo  7322  eroveu  7425  eceqoveq  7435  map0g  7478  fundmen  7609  sdomdif  7685  onsdominel  7686  nneneq  7720  php3  7723  onomeneq  7727  pssnn  7758  f1finf1o  7766  findcard3  7783  unblem1  7792  fiint  7817  ixpfi2  7838  dffi2  7903  elfiun  7910  fisup2g  7947  wemaplem2  7993  preleq  8055  inf3lem2  8067  inf3lem3  8068  inf3lem6  8071  noinfep  8097  epfrs  8183  tcmin  8193  r1sdom  8213  r1ord3g  8218  r1ord2  8220  tz9.12lem3  8228  rankelb  8263  bndrank  8280  rankunb  8289  rankuni2b  8292  cplem1  8328  karden  8334  carduni  8383  infxpenlem  8412  dfac8alem  8431  alephdom  8483  cardinfima  8499  alephval3  8512  dfac5lem4  8528  dfac5lem5  8529  dfac5  8530  dfac2  8532  kmlem13  8563  ackbij1b  8640  cfub  8650  coflim  8662  cflim2  8664  cfslbn  8668  cfslb2n  8669  cofsmo  8670  cfsmolem  8671  sornom  8678  fincssdom  8724  isf32lem1  8754  isf32lem2  8755  isf32lem9  8762  isf34lem4  8778  isfin1-3  8787  axcc4  8840  domtriomlem  8843  axdc2lem  8849  axdc3lem2  8852  zorn2lem4  8900  zorn2lem6  8902  zornn0g  8906  axdclem2  8921  uniimadom  8940  cardmin  8960  ficard  8961  konigthlem  8964  alephreg  8978  cfpwsdom  8980  axextnd  8987  fpwwe2lem6  9034  fpwwe2lem12  9040  fpwwe2lem13  9041  fpwwe2  9042  canthp1lem2  9052  winalim2  9095  tskuni  9182  grupr  9196  grur1a  9218  axgroth6  9227  grothomex  9228  eltskm  9242  addclpi  9291  nqereu  9328  ltexnq  9374  nsmallnq  9376  genpn0  9402  genpss  9403  genpnmax  9406  ltaddpr  9433  reclem3pr  9448  reclem4pr  9449  suplem1pr  9451  supsrlem  9509  1re  9616  dedekindle  9766  addid1  9781  sup2  10524  supmullem1  10534  supmullem2  10535  infmrcl  10547  zmulcl  10937  zeo  10973  uzindOLD  10982  uz11  11132  uzwo  11173  uzwoOLD  11174  eqreznegel  11196  negn0  11197  lbzbi  11199  qextlt  11431  qextle  11432  xrsupsslem  11527  xrinfmsslem  11528  supxrun  11536  supxrpnf  11539  supxrunb1  11540  supxrunb2  11541  fzm1  11787  uzrdgfni  12069  hasheqf1oi  12424  leisorel  12509  wrdsymb0  12575  swrdccatin2d  12725  repswcshw  12780  rennim  13072  sqrlem6  13081  caubnd  13191  sqreulem  13192  rlimclim  13369  caucvgrlem  13495  fsumcvg  13534  supcvg  13667  prodeq2ii  13720  fprodcvg  13737  prodmo  13743  dvdslelem  14030  bitsinv1lem  14091  bitsshft  14125  smuval2  14132  smupvallem  14133  gcdcllem1  14149  bezoutlem2  14177  bezoutlem3  14178  algcvga  14208  isprm3  14226  isprm5  14253  vdwlem13  14511  vdwnnlem1  14513  vdwnnlem3  14515  ramub1lem1  14544  imasaddfnlem  14925  divsfval  14944  catpropd  15104  joindmss  15637  meetdmss  15651  psdmrn  15837  odlem1  16559  gexlem1  16599  cygctb  16894  islss  17581  lspsneq0  17658  lspsneq  17768  mvrf1  18081  evlseu  18185  mpfrcl  18187  psgnodpmr  18626  obselocv  18759  ppttop  19508  epttop  19510  elcls  19574  restntr  19683  cnprest  19790  regsep  19835  nrmsep3  19856  lmmo  19881  cmpsublem  19899  cmpsub  19900  hauscmplem  19906  bwthOLD  19911  txcnpi  20109  txcnp  20121  fbun  20341  fbfinnfr  20342  trfbas2  20344  fgcl  20379  filssufilg  20412  ufinffr  20430  isfcls  20510  fclsrest  20525  flimfnfcls  20529  alexsubALTlem2  20548  alexsubALTlem3  20549  alexsubALTlem4  20550  alexsubALT  20551  cnextcn  20567  imasf1oxms  20992  metequiv2  21013  iccpnfcnv  21444  iccpnfhmeo  21445  iscau2  21716  caun0  21720  minveclem3b  21843  itg1climres  22121  mbfi1fseqlem4  22125  ellimc3  22283  limccnp2  22296  dvlip  22394  itgsubstlem  22449  elply2  22593  coefv0  22645  coemulc  22652  ulmss  22792  scvxcvx  23315  sqf11  23413  ppiublem1  23477  fsumvma  23488  ostth  23824  mptelee  24198  brbtwn2  24208  colinearalg  24213  axcontlem4  24270  usgrafisinds  24413  nbgra0nb  24429  nbgraf1olem5  24445  cusgrafi  24482  spthispth  24575  wlkdvspthlem  24609  usgra2adedgwlkon  24615  usgra2adedgwlkonALT  24616  4cycl4dv  24667  clwlkfclwwlk  24844  nbhashuvtx1  24915  1to3vfriendship  25008  3cyclfrgrarn1  25012  n4cyclfrgra  25018  frgrancvvdeqlemB  25038  frg2wot1  25057  frg2woteq  25060  numclwwlkun  25079  numclwwlkovf2ex  25086  numclwwlk2lem1  25102  frgraogt3nreg  25120  exidu1  25328  rngoideu  25386  zerdivemp1  25436  nmcvcn  25605  chlimi  26152  ocsh  26201  shsvs  26241  h1datomi  26499  stcl  27135  stge0  27143  stle1  27144  stm1addi  27164  stm1add3i  27166  cvnsym  27209  mdbr2  27215  dmdbr2  27222  mdsl0  27229  mdsl1i  27240  mdsl2i  27241  cvmdi  27243  atexch  27300  atcvat4i  27316  cdj1i  27352  xrge0iifcnv  27915  esumpr2  28074  sigaclci  28132  cntmeas  28197  mbfmcnt  28239  ballotlemfc0  28431  ballotlemfcc  28432  iccllyscon  28695  ghomf1olem  29034  funpsstri  29195  fundmpss  29196  fprb  29203  dfon2lem3  29217  dfon2lem4  29218  dfon2lem6  29220  dfon2lem9  29223  dfon2  29224  hbimtg  29239  hbaltg  29240  dftrpred3g  29316  poseq  29333  frrlem5b  29392  frrlem5d  29394  sltres  29424  nocvxminlem  29450  nocvxmin  29451  nofulllem5  29466  dfrdg4  29600  btwntriv2  29662  btwncomim  29663  btwnswapid  29667  btwnexch3  29670  ifscgr  29694  lineunray  29797  hilbert1.2  29805  meran3  29878  arg-ax  29881  ontopbas  29893  onsuct0  29906  limsucncmpi  29910  ordcmp  29912  onint1  29914  wl-nfeqfb  29990  wl-lem-moexsb  30017  wl-mo3t  30021  wl-ax11-lem3  30027  fin2so  30040  supadd  30042  ismblfin  30055  cldbnd  30144  tailfb  30195  indexdom  30225  fzmul  30233  heibor1lem  30305  heibor  30317  zerdivemp1x  30358  ispridl2  30435  orcomdd  30489  cnf1dd  30490  cnfn1dd  30492  cnfn2dd  30493  prtlem14  30615  prter2  30622  incssnn0  30643  fphpd  30750  rmxycomplete  30853  dford3lem1  30968  iocinico  31179  dvconstbi  31239  axc5c4c711toc7  31311  axc5c4c711to11  31312  pm14.24  31339  sbiota1  31341  fnchoice  31404  stoweidlem62  31844  2reu1  32191  ffnafv  32256  lswn0  32343  ply1mulgsumlem2  32987  bi33imp12  33259  bi123imp0  33265  ee233  33289  vk15.4j  33298  ssralv2  33301  alrim3con13v  33304  tratrb  33307  onfrALTlem3  33316  onfrALTlem2  33318  19.41rg  33323  hbimpg  33327  hbalg  33328  ax6e2ndeq  33332  e2  33417  ee223  33420  sspwtrALT  33620  sspwtrALT2  33623  suctrALT2  33637  trintALT  33681  isosctrlem1ALT  33734  bnj142OLD  33781  bnj1379  33889  bnj607  33974  bnj908  33989  bnj938  33995  bnj1174  34059  bnj1280  34076  bj-gl4  34184  bj-alrimhi  34213  bj-nalnalimiOLD  34223  bj-hbalt  34240  bj-hbsb3t  34272  bj-spimedv  34280  bj-cbv2hv  34294  bj-axc11nv  34316  bj-axc15v  34330  bj-hbsb2v  34339  bj-sbftv  34345  bj-axsep  34379  bj-equsal1t  34395  bj-bary1lem1  34680  lsatn0  34724  lsatcmp  34728  lsatcv0  34756  lfl1dim  34846  lfl1dim2N  34847  lkrss2N  34894  lub0N  34914  glb0N  34918  glbconxN  35102  hl2at  35129  cvrexchlem  35143  cvratlem  35145  cvrat4  35167  psubspi  35471  pointpsubN  35475  elpaddn0  35524  paddasslem17  35560  ispsubcl2N  35671  ldilval  35837  trlord  36295  diaelrnN  36772  cdlemm10N  36845  cdlemn11pre  36937  dihord2pre  36952  dihglblem2N  37021  dihglblem3N  37022  mapdrvallem2  37372  al3im  37766  frege60a  37905  frege60c  37950
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator