Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  3bitrrd Structured version   Visualization version   GIF version

Theorem 3bitrrd 294
 Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)
Hypotheses
Ref Expression
3bitrd.1 (𝜑 → (𝜓𝜒))
3bitrd.2 (𝜑 → (𝜒𝜃))
3bitrd.3 (𝜑 → (𝜃𝜏))
Assertion
Ref Expression
3bitrrd (𝜑 → (𝜏𝜓))

Proof of Theorem 3bitrrd
StepHypRef Expression
1 3bitrd.3 . 2 (𝜑 → (𝜃𝜏))
2 3bitrd.1 . . 3 (𝜑 → (𝜓𝜒))
3 3bitrd.2 . . 3 (𝜑 → (𝜒𝜃))
42, 3bitr2d 268 . 2 (𝜑 → (𝜃𝜓))
51, 4bitr3d 269 1 (𝜑 → (𝜏𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 196 This theorem is referenced by:  fnwelem  7179  mpt2curryd  7282  compssiso  9079  divfl0  12487  cjreb  13711  cnpart  13828  bitsuz  15034  acsfn  16143  ghmeqker  17510  odmulg  17796  psrbaglefi  19193  cnrest2  20900  hausdiag  21258  prdsbl  22106  mcubic  24374  2lgslem1a2  24915  cusgra3v  25993  areacirclem4  32673  lmclim2  32724  cmtbr2N  33558  expdiophlem1  36606  rnmpt0  38407
 Copyright terms: Public domain W3C validator