ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl5rbb Unicode version

Theorem syl5rbb 192
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 191 . 2  |-  ( ch 
->  ( ph  <->  th )
)
43bicomd 140 1  |-  ( ch 
->  ( th  <->  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  bitr3di  194  pm5.17dc  889  dn1dc  944  csbabg  3061  uniiunlem  3185  inimasn  4956  cnvpom  5081  fnresdisj  5233  f1oiso  5727  reldm  6084  mptelixpg  6628  1idprl  7405  1idpru  7406  nndiv  8768  fzn  9829  fz1sbc  9883  metrest  12685  bj-indeq  13157
  Copyright terms: Public domain W3C validator