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

Theorem 3bitrrd 309
 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 283 . 2 (𝜑 → (𝜃𝜓))
51, 4bitr3d 284 1 (𝜑 → (𝜏𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209 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 210 This theorem is referenced by:  fnwelem  7808  mpocurryd  7918  compssiso  9785  divfl0  13189  cjreb  14474  cnpart  14591  bitsuz  15813  acsfn  16922  ghmeqker  18377  odmulg  18675  psrbaglefi  20610  cnrest2  21891  hausdiag  22250  prdsbl  23098  mcubic  25433  2lgslem1a2  25974  fmptco1f1o  30392  eqg0el  30977  qsidomlem2  31037  areacirclem4  35148  lmclim2  35196  cmtbr2N  36549  expdiophlem1  39960  rnmpt0  41847  rrx2linest  45154
 Copyright terms: Public domain W3C validator