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

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

Proof of Theorem bitr2di
StepHypRef Expression
1 bitr2di.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
2 bitr2di.2 . . 3  |-  ( ch  <->  th )
31, 2bitrdi 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:  bitr4id  198  bibif  688  pm5.61  784  oranabs  805  pm5.7dc  939  nbbndc  1376  resopab2  4914  xpcom  5133  f1od2  6183  map1  6758  ac6sfi  6844  elznn0  9183  rexuz3  10894  xrmaxiflemcom  11150  metrest  12948  sincosq3sgn  13191  sincosq4sgn  13192
  Copyright terms: Public domain W3C validator