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

Theorem syl5bir 218
Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 21-Jun-1993.)
Hypotheses
Ref Expression
syl5bir.1
syl5bir.2
Assertion
Ref Expression
syl5bir

Proof of Theorem syl5bir
StepHypRef Expression
1 syl5bir.1 . . 3
21biimpri 206 . 2
3 syl5bir.2 . 2
42, 3syl5 32 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  3imtr3g  269  oplem1  964  nic-ax  1506  19.30  1692  19.33b  1696  hbnt  1894  necon1bd  2675  necon4bdOLD  2680  ssdisj  3876  pssdifn0  3888  disjss3  4451  somo  4839  frminex  4864  ordelord  4905  unizlim  4999  sofld  5460  f0rn0  5775  funopfv  5912  mpteqb  5970  suppssrOLD  6021  fvrnressn  6086  funfvima  6147  fliftfun  6210  weniso  6250  tfinds  6694  tfindsg  6695  tfindes  6697  tfinds2  6698  findsg  6727  frxp  6910  suppssr  6950  rdgsucmptnf  7114  frsucmptn  7123  tz7.49  7129  om00  7243  oewordi  7259  iiner  7402  eroveu  7425  undom  7625  sdomdif  7685  php3  7723  sucdom2  7734  unxpdomlem3  7746  fisseneq  7751  pssnn  7758  ordunifi  7790  isfinite2  7798  fiint  7817  infssuni  7831  ixpfi2  7838  finsschain  7847  ordtypelem10  7973  wofib  7991  wemapsolem  7996  unxpwdom2  8035  sucprcregOLD  8047  inf3lem2  8067  cantnfp1lem3  8120  cantnfp1  8121  cantnfp1lem3OLD  8146  cantnfp1OLD  8147  setind  8186  r1tr  8215  r1ordg  8217  rankelb  8263  rankxplim3  8320  cardlim  8374  infxpenlem  8412  infxpenc2  8420  infxpenc2OLD  8424  dfac5lem4  8528  dfac12k  8548  kmlem13  8563  sornom  8678  fin23lem25  8725  fin23lem21  8740  zorn2lem4  8900  iundom2g  8936  fpwwe2lem12  9040  fpwwe2lem13  9041  pwfseqlem4a  9060  eltsk2g  9150  inttsk  9173  tskord  9179  r1tskina  9181  grudomon  9216  arch  10817  zaddcl  10929  uzm1  11140  xrsupsslem  11527  xrinfmsslem  11528  fsequb  12085  fseqsupubi  12088  ssnn0fi  12094  seqf1o  12148  sq01  12288  swrdccatin1  12708  repsdf2  12750  cshw1  12790  rexanre  13179  rexuzre  13185  cau3lem  13187  o1co  13409  rlimcn2  13413  o1of2  13435  lo1add  13449  lo1mul  13450  climcau  13493  climbdd  13494  caucvgb  13502  summo  13539  isumltss  13660  mertenslem2  13694  prodmolem2  13742  prodmo  13743  bitsfzolem  14084  bitsfzo  14085  bezoutlem4  14179  prmind2  14228  isprm5  14253  pcqmul  14377  pcadd  14408  prmreclem2  14435  prmreclem5  14438  mul4sq  14472  vdwmc2  14497  ramcl  14547  prmlem1a  14592  divsfval  14944  iscatd2  15078  catpropd  15104  wunfunc  15268  gaorber  16346  psgneu  16531  lsmsubm  16673  pj1eu  16714  efgredlem  16765  qusabl  16871  cygabl  16893  cygctb  16894  lt6abl  16897  gsumval3eu  16907  dprdsubg  17071  ablfac1c  17122  pgpfac1  17131  dvdsrtr  17301  unitgrp  17316  drngmul0or  17417  lvecvs0or  17754  lspdisjb  17772  lspsolvlem  17788  lspprat  17799  lbsextlem2  17805  abvn0b  17951  domnchr  18569  znfld  18599  cygznlem3  18608  obselocv  18759  cpmatacl  19217  chfacfisf  19355  chfacfisfcpmat  19356  0ntr  19572  opnneiid  19627  restntr  19683  hausnei2  19854  nrmsep3  19856  cmpsub  19900  uncmp  19903  dfcon2  19920  cnconn  19923  1stcfb  19946  txuni2  20066  txbas  20068  ptbasin  20078  txcls  20105  txbasval  20107  txlly  20137  txnlly  20138  pthaus  20139  txlm  20149  tx1stc  20151  xkohaus  20154  isufil2  20409  ufileu  20420  cnpflfi  20500  txflf  20507  fclscf  20526  flimfnfcls  20529  alexsubb  20546  alexsubALTlem2  20548  alexsubALTlem4  20550  ptcmplem2  20553  ptcmplem3  20554  cnextcn  20567  qustgplem  20619  prdsmet  20873  blin2  20932  prdsbl  20994  nmolb  21224  tgqioo  21305  reconnlem2  21332  reconn  21333  lebnumlem3  21463  iscau4  21718  cmetcaulem  21727  iscmet3lem2  21731  bcthlem5  21767  minveclem3b  21843  pmltpc  21862  evthicc2  21872  ovolunlem2  21909  ovolicc2lem5  21932  mblsplit  21943  iundisj2  21959  volsup  21966  ioombl1lem4  21971  dyaddisj  22005  dyadmbllem  22008  i1faddlem  22100  itg10a  22117  itg1ge0a  22118  mbfi1flimlem  22129  mbfmullem  22132  itg2add  22166  rolle  22391  dvcvx  22421  itgsubst  22450  tdeglem4  22458  ply1domn  22524  fta1b  22570  plyadd  22614  plymul  22615  coeeu  22622  vieta1  22708  aalioulem6  22733  ulmcaulem  22789  ulmcau  22790  ulmbdd  22793  ulmcn  22794  amgm  23320  mumullem2  23454  ppiublem1  23477  dchrfi  23530  dchrptlem2  23540  dchrptlem3  23541  dchrsum2  23543  lgsdchr  23623  lgsquad2lem2  23634  2sqlem5  23643  2sqb  23653  pntlemp  23795  ostthlem2  23813  ostth  23824  tgbtwnconn1  23962  colline  24030  lmimid  24159  axcontlem8  24274  axcontlem9  24275  eengtrkg  24288  usgra2edg  24382  usg2wlkeq  24708  clwlkisclwwlklem2a4  24784  clwwisshclwwn  24808  frgraregord013  25118  nvmul0or  25547  ubthlem3  25788  axhcompl-zf  25915  hvmul0or  25942  ocnel  26216  pjhthmo  26220  spanuni  26462  spansni  26475  hon0  26712  leopadd  27051  leoptr  27056  mdsymlem6  27327  sumdmdlem2  27338  cdjreui  27351  spc2d  27373  iundisj2f  27449  disjunsn  27453  iundisj2fi  27602  ballotlemimin  28444  txscon  28686  cvmsdisj  28715  cvmliftlem15  28743  cvmlift2lem10  28757  cvmlift3lem7  28770  mclsppslem  28943  dfon2lem3  29217  dfon2lem5  29219  dfon2lem6  29220  dfon2lem7  29221  dfon2lem8  29222  soseq  29334  frr3g  29386  nodenselem4  29444  nodenselem5  29445  nobndup  29460  nobnddown  29461  ifscgr  29694  cgr3tr4  29702  btwnconn1lem13  29749  seglecgr12  29761  wl-equsal1i  29996  ismblfin  30055  itg2addnclem3  30068  ftc1anclem6  30095  elicc3  30135  neibastop1  30177  tailfb  30195  fdc  30238  riscer  30391  intidl  30426  ispridlc  30467  prtlem14  30615  prtlem17  30617  diophin  30706  diophun  30707  pm10.57  31276  fnchoice  31404  ellimcabssub0  31623  fourierdlem81  31970  fourierdlem93  31982  ralnralall  32294  2ffzoeq  32341  nzerooringczr  32880  ply1mulgsumlem1  32986  snlindsntor  33072  islininds2  33085  bnj23  33771  bnj594  33970  bnj849  33983  bj-sngltag  34541  bj-elid  34599  lpssat  34738  lssatle  34740  lshpkrlem6  34840  cvrnbtwn  34996  atlatmstc  35044  atlatle  35045  atlrelat1  35046  2at0mat0  35249  trlator0  35896  cdleme0moN  35950  cdlemn11pre  36937  dihord2pre  36952  dihmeetlem20N  37053  dochkrshp4  37116  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