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  3155  uniiunlem  3273  fnresdisj  5370  f1oiso  5864  reldm  6187  rdglim2  6461  mptelixpg  6869  1idpr  8669  nndiv  9802  fz1sbc  10875  grpid  14533  znleval  16524  fbunfip  17580  lmflf  17716  metcld2  18748  lgsne0  20588  isph  21416  dualded  25886  heibor1  26637  2rexfrabdioph  26980  dnwech  27248  2reu4a  28070  bnj168  29074  opltn0  30002  cvrnbtwn2  30087  cvrnbtwn4  30091  atlltn0  30118  pmapjat1  30664  dih1dimatlem  32141
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