MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl6rbb Structured version   Unicode version

Theorem syl6rbb 255
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
StepHypRef Expression
1 syl6rbb.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
2 syl6rbb.2 . . 3  |-  ( ch  <->  th )
31, 2syl6bb 254 . 2  |-  ( ph  ->  ( ps  <->  th )
)
43bicomd 194 1  |-  ( ph  ->  ( th  <->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  syl6rbbr  257  bibif  337  pm5.61  695  oranabs  831  necon4bid  2672  resopab2  5192  xpco  5416  funconstss  5850  xpopth  6390  map1  7187  ac6sfi  7353  rankr1bg  7731  alephsdom  7969  brdom7disj  8411  fpwwe2lem13  8519  nn0sub  10272  elznn0  10298  supxrbnd1  10902  supxrbnd2  10903  rexuz3  12154  smueqlem  13004  qnumdenbi  13138  lssne0  16029  pjfval2  16938  0top  17050  1stccn  17528  dscopn  18623  bcthlem1  19279  ovolgelb  19378  iblpos  19686  itgposval  19689  itgsubstlem  19934  sincosq3sgn  20410  sincosq4sgn  20411  lgsquadlem3  21142  nmoo0  22294  leop3  23630  leoptri  23641  tltnle  24192  nofulllem5  25663  dfrdg4  25797  colinearalg  25851  itgaddnclem2  26266  lzunuz  26828  2reu4a  27945  funressnfv  27970  usgreg2spot  28458  lfl1dim  29921  glbconxN  30177  2dim  30269  elpadd0  30608  dalawlem13  30682  diclspsn  31994  dihglb2  32142  dochsordN  32174
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 179
  Copyright terms: Public domain W3C validator