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

Theorem syl5rbb 182
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 181 . 2  |-  ( ch 
->  ( ph  <->  th )
)
43bicomd 129 1  |-  ( ch 
->  ( th  <->  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  syl5rbbr  184  pm5.17dc  810  dn1dc  867  csbabg  2907  uniiunlem  3028  inimasn  4741  cnvpom  4860  fnresdisj  5009  f1oiso  5465  reldm  5812  1idprl  6688  1idpru  6689  nndiv  7954  fzn  8906  fz1sbc  8958  bj-indeq  10053
  Copyright terms: Public domain W3C validator