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

Theorem syl5rbb 250
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 249 . 2  |-  ( ch 
->  ( ph  <->  th )
)
43bicomd 193 1  |-  ( ch 
->  ( th  <->  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  syl5rbbr  252  csbabg  3310  uniiunlem  3431  inimasn  5289  fnresdisj  5555  f1oiso  6071  reldm  6398  rdglim2  6690  mptelixpg  7099  1idpr  8906  nndiv  10040  fz1sbc  11124  grpid  14840  znleval  16835  fbunfip  17901  lmflf  18037  metcld2  19259  lgsne0  21117  isph  22323  ofpreima  24081  opelco3  25403  cnambfre  26255  heibor1  26519  2rexfrabdioph  26856  dnwech  27123  2reu4a  27943  bnj168  29097  ax7w14lemAUX7  29669  opltn0  29988  cvrnbtwn2  30073  cvrnbtwn4  30077  atlltn0  30104  pmapjat1  30650  dih1dimatlem  32127
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 178
  Copyright terms: Public domain W3C validator