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

Step	Hyp	Ref	Expression
1		3bitr3d.3	. 2
2		3bitr3d.1	. . 3
3		3bitr3d.2	. . 3
4	2, 3	bitr3d 255	. 2
5	1, 4	bitr3d 255	1

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