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

Theorem 3bitr3rd 284
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 255 . 2
51, 4bitr3d 255 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  wdomtr  7927  ltaddsub  9950  leaddsub  9952  eqneg  10188  sqreulem  13005  nmzsubg  15881  f1omvdconj  16111  dfod2  16226  odf1o2  16233  cyggenod  16522  lvecvscan  17368  znidomb  18187  mdetunilem9  18694  iccpnfcnv  20915  dvcvx  21892  cxple2  22542  wilthlem1  22806  lgslem1  23035  colinearalglem2  23622  axeuclidlem  23677  axcontlem7  23685  hvmulcan  24943  unopf1o  25789  ballotlemrv  27358  subfacp1lem3  27526  subfacp1lem5  27528  dvtanlem  28901  areacirclem1  28944  areacirc  28949  rmxdiophlem  29824  cdleme50eq  35036  hdmapeq0  36343  hdmap11  36347
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 185
  Copyright terms: Public domain W3C validator