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

Theorem 3bitr3rd 311
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 282 . 2 (𝜑 → (𝜒𝜃))
51, 4bitr3d 282 1 (𝜑 → (𝜏𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  wdomtr  9031  ltaddsub  11106  leaddsub  11108  eqneg  11352  sqreulem  14712  brcic  17060  nmzsubg  18249  f1omvdconj  18496  dfod2  18613  odf1o2  18620  cyggenod  18925  lvecvscan  19805  znidomb  20626  mdetunilem9  21147  iccpnfcnv  23465  dvcvx  24534  cxple2  25195  wilthlem1  25561  lgslem1  25789  colinearalglem2  26609  axeuclidlem  26664  axcontlem7  26672  fusgrfisstep  27027  hvmulcan  28765  unopf1o  29609  ballotlemrv  31665  subfacp1lem3  32315  subfacp1lem5  32317  wl-sbcom2d  34666  poimirlem26  34787  areacirclem1  34851  areacirc  34856  cdleme50eq  37546  hdmapeq0  38849  hdmap11  38853  rmxdiophlem  39479  nnsum3primesle9  43793  0ringdif  43975
  Copyright terms: Public domain W3C validator