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  705  oranabs  845  necon4bid  2667  resopab2  5143  xpco  5365  funconstss  5809  xpopth  6604  map1  7376  ac6sfi  7544  rankr1bg  7998  alephsdom  8244  brdom7disj  8686  fpwwe2lem13  8796  nn0sub  10617  elznn0  10648  supxrbnd1  11271  supxrbnd2  11272  rexuz3  12819  smueqlem  13668  qnumdenbi  13804  lssne0  16953  pjfval2  17975  0top  18429  1stccn  18908  dscopn  20007  bcthlem1  20676  ovolgelb  20804  iblpos  21111  itgposval  21114  itgsubstlem  21361  sincosq3sgn  21846  sincosq4sgn  21847  lgsquadlem3  22579  colinearalg  22978  nmoo0  24013  leop3  25351  leoptri  25362  f1od2  25847  tltnle  25945  nofulllem5  27693  dfrdg4  27827  itgaddnclem2  28292  lzunuz  28948  2reu4a  29856  funressnfv  29877  nn01to3  30030  wlklniswwlkn2  30177  rusgranumwlkb0  30414  usgreg2spot  30503  extwwlkfab  30526  numclwwlk2lem1  30538  lfl1dim  32336  glbconxN  32592  2dim  32684  elpadd0  33023  dalawlem13  33097  diclspsn  34409  dihglb2  34557  dochsordN  34589