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

Theorem syl5rbb 260
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 259 . 2  |-  ( ch 
->  ( ph  <->  th )
)
43bicomd 203 1  |-  ( ch 
->  ( th  <->  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 186
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 187
This theorem is referenced by:  syl5rbbr  262  necon1abid  2653  necon4abid  2656  uniiunlem  3529  inimasn  5243  fnresdisj  5674  f1oiso  6232  reldm  6837  rdglim2  7137  mptelixpg  7546  1idpr  9439  nndiv  10619  fz1sbc  11811  grpid  16411  znleval  18893  fbunfip  20664  lmflf  20800  metcld2  22039  lgsne0  23991  isph  26164  ofpreima  27963  eulerpartlemd  28824  bnj168  29125  opelco3  30006  wl-2sb6d  31388  cnambfre  31448  heibor1  31601  opltn0  32221  cvrnbtwn2  32306  cvrnbtwn4  32310  atlltn0  32337  pmapjat1  32883  dih1dimatlem  34362  2rexfrabdioph  35104  dnwech  35369  csbabgOLD  36658  2reu4a  37575  isrnghm  38222  rnghmval2  38225
  Copyright terms: Public domain W3C validator