ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3bitr3d GIF 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 (𝜑 → (𝜓𝜒))
3bitr3d.2 (𝜑 → (𝜓𝜃))
3bitr3d.3 (𝜑 → (𝜒𝜏))
Assertion
Ref Expression
3bitr3d (𝜑 → (𝜃𝜏))

Proof of Theorem 3bitr3d
StepHypRef Expression
1 3bitr3d.2 . . 3 (𝜑 → (𝜓𝜃))
2 3bitr3d.1 . . 3 (𝜑 → (𝜓𝜒))
31, 2bitr3d 190 . 2 (𝜑 → (𝜃𝜒))
4 3bitr3d.3 . 2 (𝜑 → (𝜒𝜏))
53, 4bitrd 188 1 (𝜑 → (𝜃𝜏))
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  3081  eloprabga  5962  ereldm  6578  mapen  6846  ordiso2  7034  subcan  8212  conjmulap  8686  ltrec  8840  divelunit  10002  fseq1m1p1  10095  fzm1  10100  qsqeqor  10631  fihashneq0  10774  hashfacen  10816  cvg1nlemcau  10993  lenegsq  11104  dvdsmod  11868  bezoutlemle  12009  rpexp  12153  qnumdenbi  12192  eulerthlemh  12231  odzdvds  12245  pcelnn  12320  grpidpropdg  12793  mndpropd  12841  mhmpropd  12857  grppropd  12893  cmnpropd  13098  ringpropd  13217  dvdsrpropdg  13316  lmodprop2d  13438  bdxmet  14004  txmetcnp  14021  cnmet  14033  lgsne0  14442  lgsabs1  14443
  Copyright terms: Public domain W3C validator