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

Theorem 3bitr3d 216
Description: Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 24-Apr-1996.)
Hypotheses
Ref Expression
3bitr3d.1  |-  ( ph  ->  ( ps  <->  ch )
)
3bitr3d.2  |-  ( ph  ->  ( ps  <->  th )
)
3bitr3d.3  |-  ( ph  ->  ( ch  <->  ta )
)
Assertion
Ref Expression
3bitr3d  |-  ( ph  ->  ( th  <->  ta )
)

Proof of Theorem 3bitr3d
StepHypRef Expression
1 3bitr3d.2 . . 3  |-  ( ph  ->  ( ps  <->  th )
)
2 3bitr3d.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2bitr3d 188 . 2  |-  ( ph  ->  ( th  <->  ch )
)
4 3bitr3d.3 . 2  |-  ( ph  ->  ( ch  <->  ta )
)
53, 4bitrd 186 1  |-  ( ph  ->  ( th  <->  ta )
)
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:  csbcomg  2952  eloprabga  5717  ereldm  6315  mapen  6542  ordiso2  6707  subcan  7716  conjmulap  8170  ltrec  8316  divelunit  9388  fseq1m1p1  9476  fzm1  9481  fihashneq0  10168  hashfacen  10206  cvg1nlemcau  10382  lenegsq  10493  dvdsmod  10945  bezoutlemle  11079  rpexp  11214  qnumdenbi  11252
  Copyright terms: Public domain W3C validator