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

Theorem syl6rbb 196
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl6rbb.1  |-  ( ph  ->  ( ps  <->  ch )
)
syl6rbb.2  |-  ( ch  <->  th )
Assertion
Ref Expression
syl6rbb  |-  ( ph  ->  ( th  <->  ps )
)

Proof of Theorem syl6rbb
StepHypRef Expression
1 syl6rbb.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
2 syl6rbb.2 . . 3  |-  ( ch  <->  th )
31, 2syl6bb 195 . 2  |-  ( ph  ->  ( ps  <->  th )
)
43bicomd 140 1  |-  ( ph  ->  ( th  <->  ps )
)
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:  syl6rbbr  198  bibif  687  pm5.61  783  oranabs  804  pm5.7dc  938  nbbndc  1372  resopab2  4861  xpcom  5080  f1od2  6125  map1  6699  ac6sfi  6785  elznn0  9062  rexuz3  10755  xrmaxiflemcom  11011  metrest  12664  sincosq3sgn  12898  sincosq4sgn  12899
  Copyright terms: Public domain W3C validator