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

Theorem 3bitr3d 218
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 190 . 2  |-  ( ph  ->  ( th  <->  ch )
)
4 3bitr3d.3 . 2  |-  ( ph  ->  ( ch  <->  ta )
)
53, 4bitrd 188 1  |-  ( ph  ->  ( th  <->  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:  csbcomg  3080  eloprabga  5961  ereldm  6577  mapen  6845  ordiso2  7033  subcan  8210  conjmulap  8684  ltrec  8838  divelunit  10000  fseq1m1p1  10092  fzm1  10097  qsqeqor  10627  fihashneq0  10769  hashfacen  10811  cvg1nlemcau  10988  lenegsq  11099  dvdsmod  11862  bezoutlemle  12003  rpexp  12147  qnumdenbi  12186  eulerthlemh  12225  odzdvds  12239  pcelnn  12314  grpidpropdg  12747  mndpropd  12795  mhmpropd  12811  grppropd  12847  cmnpropd  13051  ringpropd  13170  dvdsrpropdg  13269  bdxmet  13894  txmetcnp  13911  cnmet  13923  lgsne0  14332  lgsabs1  14333
  Copyright terms: Public domain W3C validator