Theorem syl6rbb 262

Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
syl6rbb.1	|- ( ph -> ( ps <-> ch ) )
syl6rbb.2	|- ( ch <-> th )

Assertion

Ref	Expression
syl6rbb	|- ( ph -> ( th <-> ps ) )

Proof of Theorem syl6rbb

Step	Hyp	Ref	Expression
1		syl6rbb.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2		syl6rbb.2	. . 3 |- ( ch <-> th )
3	1, 2	syl6bb 261	. 2 |- ( ph -> ( ps <-> th ) )
4	3	bicomd 201	1 |- ( ph -> ( th <-> ps ) )

Syntax hints:   -> wi 4   <-> wb 184

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

This theorem is referenced by:  syl6rbbr  264  bibif  346  pm5.61  712  oranabs  852  necon4bid  2707  resopab2  5256  xpco  5478  funconstss  5923  xpopth  6718  map1  7491  ac6sfi  7660  rankr1bg  8114  alephsdom  8360  brdom7disj  8802  fpwwe2lem13  8913  nn0sub  10734  elznn0  10765  supxrbnd1  11388  supxrbnd2  11389  rexuz3  12947  smueqlem  13797  qnumdenbi  13933  lssne0  17147  pjfval2  18252  0top  18713  1stccn  19192  dscopn  20291  bcthlem1  20960  ovolgelb  21088  iblpos  21396  itgposval  21399  itgsubstlem  21646  sincosq3sgn  22088  sincosq4sgn  22089  lgsquadlem3  22821  colinearalg  23301  nmoo0  24336  leop3  25674  leoptri  25685  f1od2  26168  tltnle  26261  nofulllem5  27984  dfrdg4  28118  itgaddnclem2  28592  lzunuz  29247  2reu4a  30154  funressnfv  30175  nn01to3  30328  wlklniswwlkn2  30475  rusgranumwlkb0  30712  usgreg2spot  30801  extwwlkfab  30824  numclwwlk2lem1  30836  supgtoreq  30884  lfl1dim  33075  glbconxN  33331  2dim  33423  elpadd0  33762  dalawlem13  33836  diclspsn  35148  dihglb2  35296  dochsordN  35328