Theorem syl6rbb 277

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

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

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 197

This theorem is referenced by:  syl6rbbr  279  bibif  361  pm5.61  749  oranabs  901  necon4bid  2839  resopab2  5448  xpco  5675  funconstss  6335  xpopth  7207  map1  8036  ac6sfi  8204  supgtoreq  8376  rankr1bg  8666  alephsdom  8909  brdom7disj  9353  fpwwe2lem13  9464  nn0sub  11343  elznn0  11392  nn01to3  11781  supxrbnd1  12151  supxrbnd2  12152  rexuz3  14088  smueqlem  15212  qnumdenbi  15452  dfiso3  16433  lssne0  18951  pjfval2  20053  0top  20787  1stccn  21266  dscopn  22378  bcthlem1  23121  ovolgelb  23248  iblpos  23559  itgposval  23562  itgsubstlem  23811  sincosq3sgn  24252  sincosq4sgn  24253  lgsquadlem3  25107  colinearalg  25790  wlklnwwlkln2lem  26768  2pthdlem1  26826  wwlks2onsym  26851  rusgrnumwwlkb0  26866  numclwwlk2lem1  27235  nmoo0  27646  leop3  28984  leoptri  28995  f1od2  29499  tltnle  29662  dfrdg4  32058  curf  33387  poimirlem28  33437  itgaddnclem2  33469  lfl1dim  34408  glbconxN  34664  2dim  34756  elpadd0  35095  dalawlem13  35169  diclspsn  36483  dihglb2  36631  dochsordN  36663  lzunuz  37331  uneqsn  38321  ntrclskb  38367  ntrneiel2  38384  infxrbnd2  39585  2reu4a  41189  funressnfv  41208  iccpartiltu  41358