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

Theorem 3bitrrd 305
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 279 . 2 (𝜑 → (𝜃𝜓))
51, 4bitr3d 280 1 (𝜑 → (𝜏𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205
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 206
This theorem is referenced by:  rnmpt0f  6249  sbcoteq1a  8056  fnwelem  8136  mpocurryd  8275  compssiso  10404  divfl0  13830  cjreb  15114  cnpart  15231  bitsuz  16460  acsfn  17658  eqg0el  19163  ghmeqker  19223  odmulg  19540  psrbaglefi  21899  psrbaglefiOLD  21900  cnrest2  23251  hausdiag  23610  prdsbl  24461  mcubic  26844  2lgslem1a2  27388  fmptco1f1o  32519  qsidomlem2  33286  areacirclem4  37335  lmclim2  37382  cmtbr2N  38875  expdiophlem1  42589  cantnfresb  42900  rrx2linest  48006
  Copyright terms: Public domain W3C validator