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

Theorem syl5 32
Description: A syllogism rule of inference. The first premise is used to replace the second antecedent of the second premise. (Contributed by NM, 27-Dec-1992.) (Proof shortened by Wolf Lammen, 25-May-2013.)
Hypotheses
Ref Expression
syl5.1
syl5.2
Assertion
Ref Expression
syl5

Proof of Theorem syl5
StepHypRef Expression
1 syl5.1 . . 3
2 syl5.2 . . 3
31, 2syl5com 30 . 2
43com12 31 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  syl56  34  syl2im  38  imim12i  57  pm2.86d  99  con2d  115  con3d  133  nsyli  141  syl5bi  217  syl5bir  218  syl5ib  219  adantld  467  adantrd  468  mpan9  469  pm4.79  583  pm2.36  843  pm4.72  876  ecased  944  ecase3ad  945  syl3an2  1262  alrimdh  1672  19.21v  1729  equviniv  1803  ax12w  1829  ax13dgen2  1834  ax12v  1855  ax12vOLD  1856  axc4  1860  spsd  1867  equs5e  1979  axc9lem1  2001  nfeqf  2045  hbae  2055  ax12vALT  2171  2ax6elem  2193  ax4  2225  hbae-o  2232  dvelimf-o  2259  ax12indn  2273  ax12inda2  2277  ax12a2-o  2280  euimmo  2343  necon2ad  2670  necon4ad  2677  spcimgft  3185  rr19.28v  3242  moeq3  3276  mob2  3279  euind  3286  reuind  3303  sbeqalb  3384  sbcimdvOLD  3397  triun  4558  csbexg  4584  csbexgOLD  4586  reusv2lem2  4654  ralxfrd  4666  ralxfrALT  4671  copsexg  4737  copsexgOLD  4738  pwssun  4791  somo  4839  tz7.7  4909  ordunidif  4931  trsuc  4967  trsucss  4968  suc11  4986  relssres  5316  issref  5385  dmsnopg  5484  dfco2a  5512  imadif  5668  fvelima  5925  dffv2  5946  fvmptdf  5967  fvmptf  5972  fvmptnf  5973  foco2  6051  fconst5  6128  funfvima2  6148  funfvima3  6149  isores3  6231  riotaxfrd  6288  oprabid  6323  ovmpt4g  6425  ovmpt2s  6426  ov2gf  6427  ovmpt2df  6434  suppss2OLD  6530  suppssfvOLD  6531  suppssov1OLD  6532  sorpsscmpl  6591  onint  6630  limuni3  6687  tfi  6688  tfis  6689  tfinds  6694  limomss  6705  peano5  6723  fo2ndf  6907  frxp  6910  suppssov1  6951  suppss2  6953  suppssfv  6955  rntpos  6987  tposf2  6998  onfununi  7031  smofvon2  7046  smo11  7054  smoord  7055  tfrlem11  7076  tz7.44-2  7092  tz7.48lem  7125  tz7.48-1  7127  tz7.49  7129  tz7.49c  7130  omordi  7234  omord  7236  omass  7248  oneo  7249  omeulem1  7250  omopth2  7252  oewordri  7260  oeworde  7261  nnmordi  7299  nnmord  7300  omabs  7315  nnneo  7319  omsmo  7322  ectocld  7397  qsel  7409  eceqoveq  7435  mapsn  7480  f1oeng  7554  domunsncan  7637  sbthlem1  7647  2pwuninel  7692  mapen  7701  infensuc  7715  nneneq  7720  sucdom2  7734  pssnn  7758  dif1enOLD  7772  dif1en  7773  findcard2  7780  ac6sfi  7784  frfi  7785  unblem1  7792  unblem2  7793  unbnn2  7797  nnsdomg  7799  xpfi  7811  domunfican  7813  fiint  7817  fodomfi  7819  ixpfi2  7838  finsschain  7847  marypha1lem  7913  oiexg  7981  brwdom3  8029  sucprcregOLD  8047  inf3lem2  8067  inf3lem3  8068  noinfepOLD  8098  cantnfval2  8109  cantnflt  8112  cantnflem1  8129  cantnf  8133  cantnfval2OLD  8139  cantnfltOLD  8142  cantnflem1OLD  8152  cantnfOLD  8155  cnfcom  8165  cnfcomOLD  8173  trcl  8180  epfrs  8183  r1sdom  8213  rankwflemb  8232  rankpwi  8262  rankelb  8263  carden2a  8368  cardsdomel  8376  carduni  8383  harval2  8399  pr2ne  8404  infpwfien  8464  cardaleph  8491  carduniima  8498  alephval3  8512  dfac5  8530  dfac12r  8547  dfac12k  8548  kmlem4  8554  kmlem11  8561  kmlem12  8562  cdainf  8593  infxp  8616  cfsuc  8658  cfcoflem  8673  coftr  8674  cfcof  8675  infpssr  8709  fin23lem30  8743  isf32lem1  8754  isf34lem6  8781  fin1a2lem13  8813  fin1a2s  8815  axcc2lem  8837  domtriomlem  8843  axdc4lem  8856  axcclem  8858  ac6num  8880  zorn2lem5  8901  zorn2lem6  8902  axdclem2  8921  alephval2  8968  alephreg  8978  pwcfsdom  8979  axpowndlem3OLD  8997  axregndlem1  9000  axregnd  9002  axregndOLD  9003  axacndlem1  9006  axacndlem2  9007  axacndlem3  9008  axacndlem4  9009  axacnd  9011  gchi  9023  fpwwe2lem13  9041  canthp1  9053  gchpwdom  9069  wunfi  9120  tskwe2  9172  inar1  9174  gruen  9211  intgru  9213  indpi  9306  nqereu  9328  ltbtwnnq  9377  prnmadd  9396  genpcd  9405  prlem934  9432  ltexprlem1  9435  ltexprlem2  9436  ltexprlem7  9441  ltaprlem  9443  ltapr  9444  reclem4pr  9449  suplem2pr  9452  mulcmpblnr  9469  recexsrlem  9501  mulgt0sr  9503  recexsr  9505  supsrlem  9509  axpre-sup  9567  1re  9616  dedekindle  9766  recex  10206  nnunb  10816  0mnnnnn0  10853  prime  10968  zeo  10973  fnn0ind  10988  zindd  10990  btwnz  10991  lbzbi  11199  xrub  11532  elfznelfzo  11915  facwordi  12367  fiinfnf1o  12423  hashclb  12430  hashdom  12447  hashf1lem2  12505  seqcoll  12512  hash2pwpr  12519  swrdccatin12lem2a  12710  limsupbnd2  13306  rlimdm  13374  o1of2  13435  rlimno1  13476  isercoll  13490  climcau  13493  caurcvg2  13500  caucvgb  13502  serf0  13503  zsum  13540  fsum2dlem  13585  fsum2d  13586  fsumabs  13615  fsumrlim  13625  fsumo1  13626  fsumiun  13635  incexclem  13648  zprod  13744  fprod2dlem  13784  fprod2d  13785  odd2np1  14046  ndvdssub  14065  nprm  14231  maxprmfct  14254  rpexp  14261  pc2dvds  14402  pcfac  14418  unbenlem  14426  4sqlem12  14474  4sqlem17  14479  vdwlem6  14504  vdwlem13  14511  prmlem0  14591  xpscfv  14959  mreiincl  14993  sscfn1  15186  pospo  15603  cnvpsb  15843  dirref  15865  dirtr  15866  gaass  16335  cntz2ss  16370  elsymgbas  16407  symgfix2  16441  pmtrfrn  16483  psgnran  16540  odmulg  16578  odhash3  16596  sylow2alem1  16637  sylow2alem2  16638  pj1eu  16714  efgs1b  16754  efgsfo  16757  efgredlemc  16763  efgredeu  16770  frgpuptinv  16789  lt6abl  16897  ghmcyg  16898  ablfac1eulem  17123  pgpfac1lem5  17130  irredn1  17355  irredmul  17358  lspextmo  17702  lspsncv0  17792  mplcoe1  18127  mplcoe5  18131  mplcoe2OLD  18133  evlseu  18185  cygth  18610  psgnghm  18616  mdetunilem7  19120  mdetunilem9  19122  chcoeffeq  19387  cnpco  19768  cnindis  19793  lmss  19799  lmcls  19803  lmcnp  19805  hausnei  19829  cmpsub  19900  tgcmp  19901  fiuncmp  19904  cmpfi  19908  bwth  19910  1stcrest  19954  2ndcdisj  19957  1stccnp  19963  comppfsc  20033  1stckgenlem  20054  txcls  20105  txcn  20127  txlm  20149  tx1stc  20151  txkgen  20153  xkococn  20161  hmphdis  20297  ptcmpfi  20314  isfild  20359  fgss2  20375  filcon  20384  trfil2  20388  ufileu  20420  filufint  20421  elfm2  20449  flftg  20497  cnpflf2  20501  fclssscls  20519  fclscf  20526  ufilcmp  20533  cnpfcf  20542  alexsubb  20546  alexsubALTlem4  20550  alexsubALT  20551  cnextcn  20567  qustgpopn  20618  tsmsxp  20657  isust  20706  xmettri2  20843  blin2  20932  setsmstopn  20981  met2ndc  21026  metcnp3  21043  tngtopn  21164  reconnlem2  21332  xrge0tsms  21339  fsumcn  21374  bndth  21458  iscmet3lem2  21731  iscmet3  21732  ivthlem1  21863  ivthlem2  21864  ivthlem3  21865  ovolfiniun  21912  volfiniun  21957  ioombl1lem4  21971  dyadmbl  22009  ismbf3d  22061  itg1addlem4  22106  mbfi1flimlem  22129  itg2seq  22149  itgfsum  22233  ellimc3  22283  dvmptfsum  22376  c1liplem1  22397  plypf1  22609  plydivex  22693  aannenlem1  22724  ulmval  22775  ulmcau  22790  ulmss  22792  ulmbdd  22793  ulmcn  22794  ulmdvlem3  22797  pserulm  22817  sineq0  22914  efopn  23039  cxpeq  23131  rlimcnp  23295  xrlimcnp  23298  perfectlem2  23505  lgsdir2lem2  23599  lgsne0  23608  2sqlem6  23644  2sqlem10  23649  dchrisumlem2  23675  axlowdimlem16  24260  axcontlem2  24268  usgrcyclnl1  24640  4cycl4dv  24667  el2wlkonot  24869  2wlkonot3v  24875  2spthonot3v  24876  cusgraiffrusgra  24940  2pthfrgra  25011  isgrpo  25198  grpoidinvlem3  25208  gxcom  25271  gxinv  25272  gxid  25275  gxdi  25298  opidonOLD  25324  exidu1  25328  rngoideu  25386  rngodi  25387  rngodir  25388  rngmgmbs4  25419  rngoridfz  25437  vcdi  25445  vcdir  25446  vcass  25447  nvs  25565  nvtri  25573  blocnilem  25719  chintcli  26249  hsupss  26259  shlej1  26278  elspansn4  26491  spansncvi  26570  hoaddsub  26735  lnopl  26833  lnfnl  26850  riesz4i  26982  pjnormssi  27087  pj3si  27126  stlei  27159  stcltr2i  27194  dmdmd  27219  dmdbr5  27227  mdslmd1lem2  27245  atssma  27297  atcvatlem  27304  chirredlem1  27309  atcvat4i  27316  mdsymlem2  27323  mdsymlem6  27327  sumdmdlem2  27338  dmdbr5ati  27341  cdjreui  27351  elimifd  27421  disjxpin  27447  suppss2f  27477  unifi3  27528  xrge0infss  27580  gsumle  27770  gsumvsca1  27773  gsumvsca2  27774  xrge0tsmsd  27775  lmxrge0  27934  ismeas  28170  eulerpartlemb  28307  conpcon  28680  cvmseu  28721  cvmliftlem15  28743  cvmlift2lem1  28747  cvmlift2lem12  28759  mclsind  28930  ghomf1olem  29034  dfpo2  29184  fundmpss  29196  dfon2lem3  29217  dfon2lem4  29218  dfon2lem6  29220  dfon2lem8  29222  dfon2lem9  29223  hbntg  29238  tfisg  29284  wfisg  29289  dftrpred3g  29316  trpredrec  29321  frinsg  29325  soseq  29334  wfr3g  29342  wfrlem4  29346  wfrlem5  29347  frr3g  29386  frrlem4  29390  frrlem5  29391  sltval2  29416  nodenselem5  29445  cgrdegen  29654  funtransport  29681  ifscgr  29694  cgrxfr  29705  brofs2  29727  brifs2  29728  idinside  29734  btwnconn1lem7  29743  btwnconn1lem11  29747  btwnconn1lem12  29748  btwnconn1lem14  29750  broutsideof2  29772  btwnoutside  29775  outsideoftr  29779  ontgval  29896  ordtop  29901  ordcmp  29912  onint1  29914  wl-sbcom2d  30011  wl-ax11-lem3  30027  wl-ax11-lem8  30032  tan2h  30047  ptrest  30048  heicant  30049  voliunnfl  30058  volsupnfl  30059  itg2addnclem2  30067  itg2addnc  30069  itg2gt0cn  30070  ftc2nc  30099  finminlem  30136  ntruni  30145  neibastop1  30177  filbcmb  30231  sdclem2  30235  seqpo  30240  nninfnub  30244  neificl  30246  prdstotbnd  30290  cnpwstotbnd  30293  heibor1lem  30305  heibor  30317  bfplem2  30319  grpokerinj  30347  divrngidl  30425  prnc  30464  prter2  30622  isnacs3  30642  pellexlem5  30769  pellex  30771  jm2.18  30930  jm2.15nn0  30945  jm2.16nn0  30946  setindtr  30966  dford3lem2  30969  ttac  30978  acsfn1p  31148  nzss  31222  pm11.71  31303  axc11next  31313  reuimrmo  32183  afvelima  32252  rlimdmafv  32262  ralxfrd2  32303  uhg0v  32377  copisnmnd  32497  initoid  32611  termoid  32612  funcestrcsetclem8  32653  funcsetcestrclem8  32668  rnghmsscmap2  32781  rnghmsscmap  32782  rhmsscmap2  32827  rhmsscmap  32828  funcringcsetcOLD2lem8  32851  funcringcsetclem8OLD  32874  lindslinindsimp2lem5  33063  aacllem  33216  hbntal  33326  eel2221  33489  eel2122old  33513  bnj849  33983  bnj1110  34038  bj-ax12w  34236  bj-axc15v  34330  bj-ax12v  34348  bj-hbaeb2  34391  bj-sngltag  34541  bj-xtagex  34547  bj-inftyexpiinj  34612  bj-lsub  34671  l1cvpat  34779  atcvrj0  35152  pmaple  35485  paddasslem5  35548  pclfinN  35624  osumcllem11N  35690  pexmidlem8N  35701  dvheveccl  36839  dihord6apre  36983  lpolconN  37214  rp-isfinite5  37743
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator