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

Theorem 3bitr3rd 302
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 273 . 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:  wdomtr  8720  ltaddsub  10792  leaddsub  10794  eqneg  11035  sqreulem  14437  brcic  16769  nmzsubg  17945  f1omvdconj  18175  dfod2  18291  odf1o2  18298  cyggenod  18598  lvecvscan  19429  znidomb  20228  mdetunilem9  20749  iccpnfcnv  23068  dvcvx  24121  cxple2  24781  wilthlem1  25143  lgslem1  25371  colinearalglem2  26136  axeuclidlem  26191  axcontlem7  26199  fusgrfisstep  26555  hvmulcan  28446  unopf1o  29292  ballotlemrv  31090  subfacp1lem3  31673  subfacp1lem5  31675  wl-sbcom2d  33826  poimirlem26  33916  areacirclem1  33980  areacirc  33985  cdleme50eq  36554  hdmapeq0  37857  hdmap11  37861  rmxdiophlem  38355  nnsum3primesle9  42452  0ringdif  42657
  Copyright terms: Public domain W3C validator