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

Theorem syl5rbb 258
Description: A syllogism inference from two biconditionals. (Contributed by NM, 1-Aug-1993.)
Hypotheses
Ref Expression
syl5rbb.1  |-  ( ph  <->  ps )
syl5rbb.2  |-  ( ch 
->  ( ps  <->  th )
)
Assertion
Ref Expression
syl5rbb  |-  ( ch 
->  ( th  <->  ph ) )

Proof of Theorem syl5rbb
StepHypRef Expression
1 syl5rbb.1 . . 3  |-  ( ph  <->  ps )
2 syl5rbb.2 . . 3  |-  ( ch 
->  ( ps  <->  th )
)
31, 2syl5bb 257 . 2  |-  ( ch 
->  ( ph  <->  th )
)
43bicomd 201 1  |-  ( ch 
->  ( th  <->  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  syl5rbbr  260  uniiunlem  3443  csbabgOLD  3711  inimasn  5257  fnresdisj  5524  f1oiso  6045  reldm  6628  rdglim2  6891  mptelixpg  7303  1idpr  9201  nndiv  10365  fz1sbc  11539  grpid  15576  znleval  17990  fbunfip  19445  lmflf  19581  metcld2  20820  lgsne0  22675  isph  24225  ofpreima  25987  eulerpartlemd  26752  opelco3  27592  wl-2sb6d  28387  cnambfre  28443  heibor1  28712  2rexfrabdioph  29137  dnwech  29404  2reu4a  30016  bnj168  31724  opltn0  32838  cvrnbtwn2  32923  cvrnbtwn4  32927  atlltn0  32954  pmapjat1  33500  dih1dimatlem  34977
  Copyright terms: Public domain W3C validator