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, 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 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  uniiunlem  3428  csbabgOLD  3696  inimasn  5242  fnresdisj  5509  f1oiso  6029  reldm  6614  rdglim2  6874  mptelixpg  7288  1idpr  9186  nndiv  10350  fz1sbc  11520  grpid  15553  znleval  17829  fbunfip  19284  lmflf  19420  metcld2  20659  lgsne0  22557  isph  24045  ofpreima  25808  eulerpartlemd  26597  opelco3  27436  wl-2sb6d  28232  cnambfre  28284  heibor1  28553  2rexfrabdioph  28979  dnwech  29246  2reu4a  29859  bnj168  31423  opltn0  32408  cvrnbtwn2  32493  cvrnbtwn4  32497  atlltn0  32524  pmapjat1  33070  dih1dimatlem  34547
  Copyright terms: Public domain W3C validator