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  856  necon4bid  2702  resopab2  5312  xpco  5537  funconstss  5990  xpopth  6824  map1  7596  ac6sfi  7766  supgtoreq  7931  rankr1bg  8224  alephsdom  8470  brdom7disj  8912  fpwwe2lem13  9023  nn0sub  10852  elznn0  10885  nn01to3  11184  supxrbnd1  11522  supxrbnd2  11523  rexuz3  13160  smueqlem  14017  qnumdenbi  14154  lssne0  17471  pjfval2  18613  0top  19358  1stccn  19837  dscopn  20967  bcthlem1  21636  ovolgelb  21764  iblpos  22072  itgposval  22075  itgsubstlem  22322  sincosq3sgn  22765  sincosq4sgn  22766  lgsquadlem3  23503  colinearalg  24085  wlklniswwlkn2  24572  rusgranumwlkb0  24825  usgreg2spot  24939  extwwlkfab  24962  numclwwlk2lem1  24974  nmoo0  25578  leop3  26916  leoptri  26927  f1od2  27419  tltnle  27523  nofulllem5  29441  dfrdg4  29575  itgaddnclem2  30049  lzunuz  30676  2reu4a  32032  funressnfv  32051  lfl1dim  34580  glbconxN  34836  2dim  34928  elpadd0  35267  dalawlem13  35341  diclspsn  36655  dihglb2  36803  dochsordN  36835