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

Theorem syl5rbb 191
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 190 . 2  |-  ( ch 
->  ( ph  <->  th )
)
43bicomd 139 1  |-  ( ch 
->  ( th  <->  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  syl5rbbr  193  pm5.17dc  848  dn1dc  906  csbabg  2987  uniiunlem  3107  inimasn  4836  cnvpom  4960  fnresdisj  5110  f1oiso  5587  reldm  5938  1idprl  7128  1idpru  7129  nndiv  8434  fzn  9425  fz1sbc  9477  bj-indeq  11481
  Copyright terms: Public domain W3C validator