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

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

Proof of Theorem 3bitr3rd
StepHypRef Expression
1 3bitr3d.3 . 2 (𝜑 → (𝜒𝜏))
2 3bitr3d.1 . . 3 (𝜑 → (𝜓𝜒))
3 3bitr3d.2 . . 3 (𝜑 → (𝜓𝜃))
42, 3bitr3d 281 . 2 (𝜑 → (𝜒𝜃))
51, 4bitr3d 281 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:  wdomtr  9576  ltaddsub  11695  leaddsub  11697  eqneg  11941  sqreulem  15313  brcic  17752  nmzsubg  19088  f1omvdconj  19362  dfod2  19480  odf1o2  19489  cyggenod  19800  0ringdif  20423  lvecvscan  20957  znidomb  21426  mdetunilem9  22441  iccpnfcnv  24788  dvcvx  25872  cxple2  26544  wilthlem1  26912  lgslem1  27142  colinearalglem2  28597  axeuclidlem  28652  axcontlem7  28660  fusgrfisstep  29018  hvmulcan  30757  unopf1o  31601  ballotlemrv  33981  subfacp1lem3  34636  subfacp1lem5  34638  wl-sbcom2d  36889  poimirlem26  36977  areacirclem1  37039  areacirc  37044  cdleme50eq  39875  hdmapeq0  41178  hdmap11  41182  rmxdiophlem  42216  ordeldif1o  42472  nnsum3primesle9  46920
  Copyright terms: Public domain W3C validator