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

Theorem 3bitrrd 298
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 272 . 2 (𝜑 → (𝜃𝜓))
51, 4bitr3d 273 1 (𝜑 → (𝜏𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198
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 199
This theorem is referenced by:  fnwelem  7623  mpocurryd  7731  compssiso  9586  divfl0  13002  cjreb  14333  cnpart  14450  bitsuz  15673  acsfn  16778  ghmeqker  18146  odmulg  18434  psrbaglefi  19856  cnrest2  21588  hausdiag  21947  prdsbl  22794  mcubic  25116  2lgslem1a2  25658  fmptco1f1o  30130  areacirclem4  34374  lmclim2  34423  cmtbr2N  35782  expdiophlem1  38959  rnmpt0  40854  rrx2linest  44037
  Copyright terms: Public domain W3C validator