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

Theorem syl5ibr 221
Description: A mixed syllogism inference. (Contributed by NM, 3-Apr-1994.)
Hypotheses
Ref Expression
syl5ibr.1
syl5ibr.2
Assertion
Ref Expression
syl5ibr

Proof of Theorem syl5ibr
StepHypRef Expression
1 syl5ibr.1 . 2
2 syl5ibr.2 . . 3
32bicomd 201 . 2
41, 3syl5ib 219 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  syl5ibrcom  222  biimprd  223  exdistrf  2075  pm2.61ne  2772  pm2.61neOLD  2773  unineq  3747  oteqex  4745  ordtri3  4919  limelon  4946  otel3xp  5040  elrnmpt1  5256  cnveqb  5467  cnveq0  5468  relcoi1  5541  ndmfv  5895  ffvresb  6062  isomin  6233  isofrlem  6236  caovord3d  6485  eldifpw  6612  ssonuni  6622  onsucuni2  6669  ordzsl  6680  tfindsg  6695  findsg  6727  oteqimp  6819  frxp  6910  poxp  6912  fnwelem  6915  suppss  6949  tfrlem11  7076  oacl  7204  omcl  7205  oecl  7206  oa0r  7207  om0r  7208  om1r  7211  oe1m  7213  oaordi  7214  oawordri  7218  oaass  7229  oarec  7230  omwordri  7240  odi  7247  omass  7248  oewordri  7260  oeworde  7261  oeordsuc  7262  oelim2  7263  oeoa  7265  oeoelem  7266  oeoe  7267  nnm0r  7278  nnacl  7279  nnacom  7285  nnaordi  7286  nnaass  7290  nndi  7291  nnmass  7292  nnmsucr  7293  nnmcom  7294  omabs  7315  brecop  7423  eceqoveq  7435  elpm2r  7456  map0g  7478  undifixp  7525  fundmen  7609  mapxpen  7703  mapunen  7706  php  7721  unxpdomlem2  7745  pssnn  7758  elfir  7895  wemapso2OLD  7998  wemapso2lem  7999  wdompwdom  8025  inf3lem1  8066  inf3lem3  8068  noinfepOLD  8098  cantnfval2  8109  cantnfp1lem3  8120  cantnfval2OLD  8139  cantnfp1lem3OLD  8146  r1sdom  8213  r1tr  8215  carden2a  8368  fidomtri2  8396  prdom2  8405  infxpenlem  8412  acndom  8453  fodomacn  8458  wdomfil  8463  alephon  8471  alephordi  8476  alephle  8490  alephfplem3  8508  dfac2a  8531  kmlem9  8559  cflm  8651  cfslb  8667  cfslbn  8668  infpssrlem3  8706  infpssrlem4  8707  fin23lem21  8740  fin23lem30  8743  isf34lem7  8780  isf34lem6  8781  fin67  8796  isfin7-2  8797  fin1a2lem7  8807  fin1a2lem10  8810  iundom2g  8936  konigthlem  8964  alephreg  8978  gchdomtri  9028  wunr1om  9118  tskr1om  9166  inar1  9174  grur1a  9218  indpi  9306  genpprecl  9400  genpnmax  9406  addcmpblnr  9467  recexsrlem  9501  map2psrpr  9508  ax1rid  9559  axpre-mulgt0  9566  ltle  9694  nnmulcl  10584  nnsub  10599  nn0sub  10871  nneo  10971  uzindOLD  10982  uz11  11132  xrltle  11384  xltnegi  11444  xrsupsslem  11527  xrinfmsslem  11528  xrub  11532  supxrunb1  11540  supxrunb2  11541  om2uzuzi  12060  uzrdgxfr  12077  seqcl2  12125  seqfveq2  12129  seqshft2  12133  seqsplit  12140  seqcaopr3  12142  seqf1olem2a  12145  seqid2  12153  seqhomo  12154  ser1const  12163  m1expcl2  12188  expadd  12208  expmul  12211  faclbnd  12368  hashmap  12493  hashfacen  12503  hashf1lem1  12504  hashf1lem2  12505  hashf1  12506  seqcoll  12512  wrdsymb0  12575  lsw0  12586  swrdvalodm2  12664  swrdvalodm  12665  wrd2ind  12703  swrdccatin12lem2  12714  swrdccatin1d  12724  repswccat  12757  repswcshw  12780  cshwcshid  12795  recan  13169  rexanre  13179  rlimcn2  13413  caurcvg2  13500  fsumiun  13635  efexp  13836  rpnnen2  13959  dvdstr  14018  alzdvds  14036  bitsinv1  14092  smu01lem  14135  smupval  14138  smueqlem  14140  smumullem  14142  seq1st  14200  prmdiveq  14316  odzdvds  14322  pythagtriplem2  14341  pcexp  14383  vdwlem13  14511  ramz  14543  elrestr  14826  xpsff1o  14965  subsubc  15222  clatl  15746  frmdgsum  16030  mulgneg2  16169  mulgnnass  16170  mhmmulg  16174  gsumwrev  16401  symgbas  16405  symgextf1lem  16445  symgfixelsi  16460  pmtrdifellem4  16504  sylow1lem1  16618  efgsfo  16757  efgred  16766  cyggexb  16901  gsumzres  16914  gsum2dlem2  16998  gsum2dOLD  17000  mulgass2  17247  lmodprop2d  17572  lspsnne2  17764  lspsneu  17769  assapropd  17976  mplcoe1  18127  mplcoe3  18128  mplcoe3OLD  18129  mplcoe5  18131  mplcoe2OLD  18133  ply1sclf1  18330  cnfldmulg  18450  cnfldexp  18451  zrhpsgnelbas  18630  mat1scmat  19041  restopn2  19678  cnpf2  19751  cmpfi  19908  txcn  20127  txlm  20149  xkoptsub  20155  xkopjcn  20157  ufildr  20432  cnflf  20503  fclsnei  20520  fclscmp  20531  ufilcmp  20533  cnfcf  20543  symgtgp  20600  isxms2  20951  met2ndc  21026  metustblOLD  21083  metustbl  21084  tngngp2  21166  clmmulg  21593  iscau4  21718  ovolunlem1a  21907  ovolicc2lem4  21931  volfiniun  21957  voliunlem1  21960  volsup  21966  dvnadd  22332  dvnres  22334  dvcobr  22349  ply1nzb  22523  plypf1  22609  dgrle  22640  coeaddlem  22646  dgrlt  22663  dvntaylp  22766  cxpmul2  23070  rlimcnp  23295  wilthlem2  23343  isnsqf  23409  musum  23467  chtub  23487  chpval2  23493  dchrisumlem1  23674  qabvexp  23811  ostthlem2  23813  axsegconlem1  24220  ax5seglem4  24235  ax5seglem5  24236  axlowdimlem15  24259  axcontlem2  24268  axcontlem4  24270  ushgrauhgra  24303  usgra2edg  24382  cusgrafilem1  24479  sizeusglecusglem1  24484  sizeusglecusg  24486  trliswlk  24541  2trllemF  24551  constr3lem6  24649  1conngra  24675  wlkiswwlk2lem4  24694  wwlknredwwlkn0  24727  wwlkextwrd  24728  wwlkextproplem1  24741  wwlkextprop  24744  clwlkisclwwlklem2a  24785  clwwlkf1  24796  erclwwlksym  24814  eleclclwwlknlem2  24818  erclwwlknsym  24826  el2wlkonot  24869  el2spthonot  24870  hashnbgravdg  24913  eupatrl  24968  frgra3vlem1  25000  3vfriswmgralem  25004  frconngra  25021  frgrawopreglem3  25046  frg2wot1  25057  2spotiundisj  25062  usg2spot2nb  25065  usgreg2spot  25067  extwwlkfablem2  25078  numclwwlkovf2ex  25086  extwwlkfab  25090  isexid2  25327  ismndo1  25346  rngo2  25390  rngoueqz  25432  sspval  25636  nmosetre  25679  nmobndseqi  25694  nmobndseqiOLD  25695  orthcom  26025  shsva  26238  shmodsi  26307  h1datomi  26499  nmopsetretALT  26782  nmfnsetre  26796  lnopcnbd  26955  pjclem4  27118  pj3si  27126  ssmd1  27230  atom1d  27272  chjatom  27276  atcvat4i  27316  cdj3lem2a  27355  cdj3lem3a  27358  disjunsn  27453  unitdivcld  27883  xrge0iifiso  27917  dya2iocuni  28254  facgam  28608  deranglem  28610  subfacp1lem6  28629  subfacval2  28631  cvmlift2lem12  28759  mrsubvrs  28882  msrrcl  28903  mclsax  28929  relexpsucr  29053  relexpsucl  29055  relexprel  29057  relexpdm  29058  relexprn  29059  relexpadd  29061  relexpindlem  29062  relexpind  29063  rtrclreclem.trans  29069  rtrclreclem.min  29070  dfrtrcl2  29071  rtrclind  29072  dfon2lem6  29220  rdgprc  29227  predpoirr  29277  predfrirr  29278  trpredlem1  29310  wfrlem14  29356  frrlem5e  29395  nodenselem8  29448  ifscgr  29694  btwncolinear1  29719  hfelhf  29838  ordcmp  29912  findreccl  29918  nndivlub  29923  wl-mo3t  30021  opnrebl2  30139  nn0prpw  30141  eqfnun  30212  sdclem2  30235  sdclem1  30236  prdsbnd2  30291  ismtyval  30296  rrnequiv  30331  exidreslem  30339  risci  30390  prtlem11  30607  prtlem15  30616  aovmpt4g  32286  f1vrnfibi  32313  ushguhg  32371  funcrngcsetc  32806  funcrngcsetcALT  32807  rhmsscrnghm  32834  funcringcsetc  32843  ellcoellss  33036  bnj168  33785  bnj535  33948  bnj590  33968  bnj594  33970  bnj938  33995  bnj1118  34040  bnj1128  34046  cvrat4  35167  lcfl6  37227
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
  Copyright terms: Public domain W3C validator