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 280 . 2 (𝜑 → (𝜒𝜃))
51, 4bitr3d 280 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  9334  ltaddsub  11449  leaddsub  11451  eqneg  11695  sqreulem  15071  brcic  17510  nmzsubg  18793  f1omvdconj  19054  dfod2  19171  odf1o2  19178  cyggenod  19484  lvecvscan  20373  znidomb  20769  mdetunilem9  21769  iccpnfcnv  24107  dvcvx  25184  cxple2  25852  wilthlem1  26217  lgslem1  26445  colinearalglem2  27275  axeuclidlem  27330  axcontlem7  27338  fusgrfisstep  27696  hvmulcan  29434  unopf1o  30278  ballotlemrv  32486  subfacp1lem3  33144  subfacp1lem5  33146  wl-sbcom2d  35716  poimirlem26  35803  areacirclem1  35865  areacirc  35870  cdleme50eq  38555  hdmapeq0  39858  hdmap11  39862  rmxdiophlem  40837  nnsum3primesle9  45246  0ringdif  45428
  Copyright terms: Public domain W3C validator