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  2672  resopab2  5150  xpco  5372  funconstss  5816  xpopth  6610  map1  7380  ac6sfi  7548  rankr1bg  8002  alephsdom  8248  brdom7disj  8690  fpwwe2lem13  8801  nn0sub  10622  elznn0  10653  supxrbnd1  11276  supxrbnd2  11277  rexuz3  12828  smueqlem  13678  qnumdenbi  13814  lssne0  17009  pjfval2  18109  0top  18563  1stccn  19042  dscopn  20141  bcthlem1  20810  ovolgelb  20938  iblpos  21245  itgposval  21248  itgsubstlem  21495  sincosq3sgn  21937  sincosq4sgn  21938  lgsquadlem3  22670  colinearalg  23107  nmoo0  24142  leop3  25480  leoptri  25491  f1od2  25975  tltnle  26074  nofulllem5  27798  dfrdg4  27932  itgaddnclem2  28404  lzunuz  29059  2reu4a  29966  funressnfv  29987  nn01to3  30140  wlklniswwlkn2  30287  rusgranumwlkb0  30524  usgreg2spot  30613  extwwlkfab  30636  numclwwlk2lem1  30648  supgtoreq  30694  lfl1dim  32606  glbconxN  32862  2dim  32954  elpadd0  33293  dalawlem13  33367  diclspsn  34679  dihglb2  34827  dochsordN  34859