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

Theorem 3bitr3rd 313
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 284 . 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:  wdomtr  9112  ltaddsub  11192  leaddsub  11194  eqneg  11438  sqreulem  14809  brcic  17173  nmzsubg  18435  f1omvdconj  18692  dfod2  18809  odf1o2  18816  cyggenod  19122  lvecvscan  20002  znidomb  20380  mdetunilem9  21371  iccpnfcnv  23696  dvcvx  24772  cxple2  25440  wilthlem1  25805  lgslem1  26033  colinearalglem2  26853  axeuclidlem  26908  axcontlem7  26916  fusgrfisstep  27271  hvmulcan  29007  unopf1o  29851  ballotlemrv  32056  subfacp1lem3  32715  subfacp1lem5  32717  wl-sbcom2d  35339  poimirlem26  35426  areacirclem1  35488  areacirc  35493  cdleme50eq  38178  hdmapeq0  39481  hdmap11  39485  rmxdiophlem  40409  nnsum3primesle9  44780  0ringdif  44962
  Copyright terms: Public domain W3C validator