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

Theorem syl5rbb 249
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-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 248 . 2  |-  ( ch 
->  ( ph  <->  th )
)
43bicomd 192 1  |-  ( ch 
->  ( th  <->  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  syl5rbbr  251  csbabg  3142  uniiunlem  3260  fnresdisj  5354  f1oiso  5848  reldm  6171  rdglim2  6445  mptelixpg  6853  1idpr  8653  nndiv  9786  fz1sbc  10859  grpid  14517  znleval  16508  fbunfip  17564  lmflf  17700  metcld2  18732  lgsne0  20572  isph  21400  dualded  25783  heibor1  26534  2rexfrabdioph  26877  dnwech  27145  2reu4a  27967  bnj168  28758  opltn0  29380  cvrnbtwn2  29465  cvrnbtwn4  29469  atlltn0  29496  pmapjat1  30042  dih1dimatlem  31519
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 177
  Copyright terms: Public domain W3C validator