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  8022  ltaddsub  10051  leaddsub  10053  eqneg  10289  sqreulem  13192  nmzsubg  16242  f1omvdconj  16471  dfod2  16586  odf1o2  16593  cyggenod  16887  lvecvscan  17757  znidomb  18600  mdetunilem9  19122  iccpnfcnv  21444  dvcvx  22421  cxple2  23078  wilthlem1  23342  lgslem1  23571  colinearalglem2  24210  axeuclidlem  24265  axcontlem7  24273  hvmulcan  25989  unopf1o  26835  ballotlemrv  28458  subfacp1lem3  28626  subfacp1lem5  28628  wl-sbcom2d  30011  dvtanlem  30064  areacirclem1  30107  areacirc  30112  rmxdiophlem  30957  brcic  32582  0ringdif  32676  cdleme50eq  36267  hdmapeq0  37574  hdmap11  37578 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