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

Theorem 3bitr2d 216
Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)
Hypotheses
Ref Expression
3bitr2d.1  |-  ( ph  ->  ( ps  <->  ch )
)
3bitr2d.2  |-  ( ph  ->  ( th  <->  ch )
)
3bitr2d.3  |-  ( ph  ->  ( th  <->  ta )
)
Assertion
Ref Expression
3bitr2d  |-  ( ph  ->  ( ps  <->  ta )
)

Proof of Theorem 3bitr2d
StepHypRef Expression
1 3bitr2d.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
2 3bitr2d.2 . . 3  |-  ( ph  ->  ( th  <->  ch )
)
31, 2bitr4d 191 . 2  |-  ( ph  ->  ( ps  <->  th )
)
4 3bitr2d.3 . 2  |-  ( ph  ->  ( th  <->  ta )
)
53, 4bitrd 188 1  |-  ( ph  ->  ( ps  <->  ta )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  ceqsralt  2799  frecsuclem  6492  indpi  7455  cauappcvgprlemladdru  7769  prsrlt  7900  lesub2  8530  ltsub2  8532  rec11ap  8783  avglt1  9276  rpnegap  9808  modqmuladdnn0  10513  expap0  10714  swrdspsleq  11120  2shfti  11142  mulreap  11175  minmax  11541  lemininf  11545  xrminmax  11576  xrlemininf  11582  modremain  12240  nnwosdc  12360  nn0seqcvgd  12363  divgcdcoprm0  12423  ismgmid  13209  grpsubeq0  13418  grpsubadd  13420  eqg0el  13565  isunitd  13868  lsslss  14143  isridlrng  14244  zndvds  14411  znleval  14415  isxmet2d  14820  xblss2  14877  neibl  14963  ellimc3apf  15132  logbgt0b  15438  lgsne0  15515  lgsabs1  15516  lgsquadlem1  15554  m1lgs  15562  iswomninnlem  15988
  Copyright terms: Public domain W3C validator