Theorem syl6rbb 266

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

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

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 189

This theorem is referenced by:  syl6rbbr  268  bibif  348  pm5.61  718  oranabs  866  necon4bid  2668  resopab2  5152  xpco  5375  funconstss  5998  xpopth  6829  map1  7645  ac6sfi  7812  supgtoreq  7983  rankr1bg  8271  alephsdom  8514  brdom7disj  8956  fpwwe2lem13  9064  nn0sub  10917  elznn0  10949  nn01to3  11254  supxrbnd1  11604  supxrbnd2  11605  rexuz3  13404  smueqlem  14457  qnumdenbi  14686  dfiso3  15671  lssne0  18167  pjfval2  19265  0top  19992  1stccn  20471  dscopn  21581  bcthlem1  22285  ovolgelb  22426  iblpos  22743  itgposval  22746  itgsubstlem  22993  sincosq3sgn  23448  sincosq4sgn  23449  lgsquadlem3  24277  colinearalg  24933  wlklniswwlkn2  25421  rusgranumwlkb0  25674  usgreg2spot  25788  extwwlkfab  25811  numclwwlk2lem1  25823  nmoo0  26425  leop3  27771  leoptri  27782  f1od2  28302  tltnle  28416  nofulllem5  30588  dfrdg4  30711  poimirlem28  31961  itgaddnclem2  31994  lfl1dim  32681  glbconxN  32937  2dim  33029  elpadd0  33368  dalawlem13  33442  diclspsn  34756  dihglb2  34904  dochsordN  34936  lzunuz  35604  2reu4a  38604  funressnfv  38623  iccpartiltu  38730