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

Theorem 3bitr3rd 299
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 270 . 2 (𝜑 → (𝜒𝜃))
51, 4bitr3d 270 1 (𝜑 → (𝜏𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  wdomtr  8647  ltaddsub  10714  leaddsub  10716  eqneg  10957  sqreulem  14318  brcic  16679  nmzsubg  17856  f1omvdconj  18086  dfod2  18201  odf1o2  18208  cyggenod  18506  lvecvscan  19333  znidomb  20132  mdetunilem9  20648  iccpnfcnv  22964  dvcvx  24002  cxple2  24663  wilthlem1  25014  lgslem1  25242  colinearalglem2  26007  axeuclidlem  26062  axcontlem7  26070  fusgrfisstep  26441  hvmulcan  28259  unopf1o  29105  ballotlemrv  30911  subfacp1lem3  31492  subfacp1lem5  31494  wl-sbcom2d  33675  poimirlem26  33766  areacirclem1  33831  areacirc  33836  cdleme50eq  36349  hdmapeq0  37656  hdmap11  37660  rmxdiophlem  38102  nnsum3primesle9  42210  0ringdif  42398
  Copyright terms: Public domain W3C validator