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  necon1abid  2715  necon4abid  2718  uniiunlem  3588  csbabgOLD  3856  inimasn  5421  fnresdisj  5689  f1oiso  6233  reldm  6832  rdglim2  7095  mptelixpg  7503  1idpr  9403  nndiv  10572  fz1sbc  11750  grpid  15886  znleval  18360  fbunfip  20105  lmflf  20241  metcld2  21480  lgsne0  23336  isph  25413  ofpreima  27179  eulerpartlemd  27945  opelco3  28785  wl-2sb6d  29585  cnambfre  29640  heibor1  29909  2rexfrabdioph  30333  dnwech  30598  2reu4a  31661  bnj168  32865  opltn0  33987  cvrnbtwn2  34072  cvrnbtwn4  34076  atlltn0  34103  pmapjat1  34649  dih1dimatlem  36126
  Copyright terms: Public domain W3C validator