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

Theorem syl5rbb 262
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 261 . 2  |-  ( ch 
->  ( ph  <->  th )
)
43bicomd 205 1  |-  ( ch 
->  ( th  <->  ph ) )
Colors of variables: wff setvar class
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:  syl5rbbr  264  necon1abid  2673  necon4abid  2676  uniiunlem  3550  inimasn  5270  fnresdisj  5702  f1oiso  6255  reldm  6856  rdglim2  7156  mptelixpg  7565  1idpr  9456  nndiv  10652  fz1sbc  11872  grpid  16694  znleval  19117  fbunfip  20876  lmflf  21012  metcld2  22268  lgsne0  24253  isph  26455  ofpreima  28264  eulerpartlemd  29201  bnj168  29540  opelco3  30421  wl-2sb6d  31808  poimirlem26  31886  cnambfre  31909  heibor1  32062  opltn0  32681  cvrnbtwn2  32766  cvrnbtwn4  32770  atlltn0  32797  pmapjat1  33343  dih1dimatlem  34822  2rexfrabdioph  35564  dnwech  35832  csbabgOLD  37078  2reu4a  38329  isrnghm  39196  rnghmval2  39199
  Copyright terms: Public domain W3C validator