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

Theorem syl6rbb 262
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl6rbb.1
syl6rbb.2
Assertion
Ref Expression
syl6rbb

Proof of Theorem syl6rbb
StepHypRef Expression
1 syl6rbb.1 . . 3
2 syl6rbb.2 . . 3
31, 2syl6bb 261 . 2
43bicomd 201 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  syl6rbbr  264  bibif  346  pm5.61  712  oranabs  856  necon4bid  2716  resopab2  5327  xpco  5552  funconstss  6005  xpopth  6839  map1  7614  ac6sfi  7784  supgtoreq  7949  rankr1bg  8242  alephsdom  8488  brdom7disj  8930  fpwwe2lem13  9041  nn0sub  10871  elznn0  10904  nn01to3  11204  supxrbnd1  11542  supxrbnd2  11543  rexuz3  13181  smueqlem  14140  qnumdenbi  14277  lssne0  17597  pjfval2  18740  0top  19485  1stccn  19964  dscopn  21094  bcthlem1  21763  ovolgelb  21891  iblpos  22199  itgposval  22202  itgsubstlem  22449  sincosq3sgn  22893  sincosq4sgn  22894  lgsquadlem3  23631  colinearalg  24213  wlklniswwlkn2  24700  rusgranumwlkb0  24953  usgreg2spot  25067  extwwlkfab  25090  numclwwlk2lem1  25102  nmoo0  25706  leop3  27044  leoptri  27055  f1od2  27547  tltnle  27650  nofulllem5  29466  dfrdg4  29600  itgaddnclem2  30074  lzunuz  30701  2reu4a  32194  funressnfv  32213  dfiso3  32569  lfl1dim  34846  glbconxN  35102  2dim  35194  elpadd0  35533  dalawlem13  35607  diclspsn  36921  dihglb2  37069  dochsordN  37101
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