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

Theorem syl5rbb 266
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 265 . 2  |-  ( ch 
->  ( ph  <->  th )
)
43bicomd 206 1  |-  ( ch 
->  ( th  <->  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189
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 190
This theorem is referenced by:  syl5rbbr  268  necon1abid  2673  necon4abid  2675  uniiunlem  3528  inimasn  5271  fnresdisj  5707  f1oiso  6266  reldm  6870  rdglim2  7175  mptelixpg  7584  1idpr  9479  nndiv  10677  fz1sbc  11898  grpid  16749  znleval  19173  fbunfip  20932  lmflf  21068  metcld2  22324  lgsne0  24309  isph  26511  ofpreima  28316  eulerpartlemd  29247  bnj168  29586  opelco3  30468  wl-2sb6d  31932  poimirlem26  32010  cnambfre  32033  heibor1  32186  opltn0  32800  cvrnbtwn2  32885  cvrnbtwn4  32889  atlltn0  32916  pmapjat1  33462  dih1dimatlem  34941  2rexfrabdioph  35683  dnwech  35950  csbabgOLD  37250  2reu4a  38647  isuvtxa  39516  isrnghm  40164  rnghmval2  40167
  Copyright terms: Public domain W3C validator