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

Theorem 3bitr3d 217
 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
3bitr3d.2
3bitr3d.3
Assertion
Ref Expression
3bitr3d

Proof of Theorem 3bitr3d
StepHypRef Expression
1 3bitr3d.2 . . 3
2 3bitr3d.1 . . 3
31, 2bitr3d 189 . 2
4 3bitr3d.3 . 2
53, 4bitrd 187 1
 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:  csbcomg  3030  eloprabga  5866  ereldm  6480  mapen  6748  ordiso2  6928  subcan  8042  conjmulap  8514  ltrec  8666  divelunit  9816  fseq1m1p1  9907  fzm1  9912  fihashneq0  10574  hashfacen  10612  cvg1nlemcau  10789  lenegsq  10900  dvdsmod  11597  bezoutlemle  11733  rpexp  11868  qnumdenbi  11907  bdxmet  12710  txmetcnp  12727  cnmet  12739
 Copyright terms: Public domain W3C validator