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  9512  ltaddsub  11630  leaddsub  11632  eqneg  11876  sqreulem  15245  brcic  17682  nmzsubg  18968  f1omvdconj  19229  dfod2  19347  odf1o2  19356  cyggenod  19662  lvecvscan  20575  znidomb  20971  mdetunilem9  21972  iccpnfcnv  24310  dvcvx  25387  cxple2  26055  wilthlem1  26420  lgslem1  26648  colinearalglem2  27859  axeuclidlem  27914  axcontlem7  27922  fusgrfisstep  28280  hvmulcan  30017  unopf1o  30861  ballotlemrv  33122  subfacp1lem3  33779  subfacp1lem5  33781  wl-sbcom2d  36019  poimirlem26  36107  areacirclem1  36169  areacirc  36174  cdleme50eq  39007  hdmapeq0  40310  hdmap11  40314  rmxdiophlem  41342  ordeldif1o  41598  nnsum3primesle9  45993  0ringdif  46175
  Copyright terms: Public domain W3C validator