Theorem syl6rbb 254

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

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

This theorem is referenced by:  syl6rbbr  256  bibif  336  pm5.61  694  oranabs  830  necon4bid  2633  resopab2  5149  xpco  5373  funconstss  5807  xpopth  6347  map1  7144  ac6sfi  7310  rankr1bg  7685  alephsdom  7923  brdom7disj  8365  fpwwe2lem13  8473  nn0sub  10226  elznn0  10252  supxrbnd1  10856  supxrbnd2  10857  rexuz3  12107  smueqlem  12957  qnumdenbi  13091  lssne0  15982  pjfval2  16891  0top  17003  1stccn  17479  dscopn  18574  bcthlem1  19230  ovolgelb  19329  iblpos  19637  itgposval  19640  itgsubstlem  19885  sincosq3sgn  20361  sincosq4sgn  20362  lgsquadlem3  21093  nmoo0  22245  leop3  23581  leoptri  23592  tltnle  24143  nofulllem5  25574  dfrdg4  25703  colinearalg  25753  itgaddnclem2  26163  lzunuz  26716  2reu4a  27834  funressnfv  27859  usgreg2spot  28170  lfl1dim  29604  glbconxN  29860  2dim  29952  elpadd0  30291  dalawlem13  30365  diclspsn  31677  dihglb2  31825  dochsordN  31857

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178