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 206
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 207
This theorem is referenced by:  wdomtr  9616  ltaddsub  11738  leaddsub  11740  eqneg  11988  sqreulem  15399  brcic  17843  nmzsubg  19184  f1omvdconj  19465  dfod2  19583  odf1o2  19592  cyggenod  19903  0ringdif  20528  lvecvscan  21114  znidomb  21581  mdetunilem9  22627  iccpnfcnv  24976  dvcvx  26060  cxple2  26740  wilthlem1  27112  lgslem1  27342  colinearalglem2  28923  axeuclidlem  28978  axcontlem7  28986  fusgrfisstep  29347  hvmulcan  31092  unopf1o  31936  ballotlemrv  34523  subfacp1lem3  35188  subfacp1lem5  35190  wl-sbcom2d  37563  poimirlem26  37654  areacirclem1  37716  areacirc  37721  cdleme50eq  40544  hdmapeq0  41847  hdmap11  41851  ef11d  42380  rmxdiophlem  43032  ordeldif1o  43278  nnsum3primesle9  47786
  Copyright terms: Public domain W3C validator