Theorem syl6rbb 265

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 264	. 2 |- ( ph -> ( ps <-> th ) )
4	3	bicomd 204	1 |- ( ph -> ( th <-> ps ) )

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

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 188

This theorem is referenced by:  syl6rbbr  267  bibif  347  pm5.61  717  oranabs  864  necon4bid  2681  resopab2  5164  xpco  5387  funconstss  6006  xpopth  6837  map1  7646  ac6sfi  7812  supgtoreq  7983  rankr1bg  8264  alephsdom  8506  brdom7disj  8948  fpwwe2lem13  9056  nn0sub  10909  elznn0  10941  nn01to3  11246  supxrbnd1  11596  supxrbnd2  11597  rexuz3  13379  smueqlem  14427  qnumdenbi  14653  dfiso3  15630  lssne0  18115  pjfval2  19209  0top  19936  1stccn  20415  dscopn  21525  bcthlem1  22211  ovolgelb  22340  iblpos  22657  itgposval  22660  itgsubstlem  22907  sincosq3sgn  23359  sincosq4sgn  23360  lgsquadlem3  24186  colinearalg  24827  wlklniswwlkn2  25314  rusgranumwlkb0  25567  usgreg2spot  25681  extwwlkfab  25704  numclwwlk2lem1  25716  nmoo0  26318  leop3  27654  leoptri  27665  f1od2  28193  tltnle  28302  nofulllem5  30421  dfrdg4  30544  poimirlem28  31716  itgaddnclem2  31749  lfl1dim  32440  glbconxN  32696  2dim  32788  elpadd0  33127  dalawlem13  33201  diclspsn  34515  dihglb2  34663  dochsordN  34695  lzunuz  35363  2reu4a  38058  funressnfv  38077  iccpartiltu  38183