Theorem 3bitr2ri 274

Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.)

Hypotheses

Ref	Expression
3bitr2i.1
3bitr2i.2
3bitr2i.3

Assertion

Ref	Expression
3bitr2ri

Proof of Theorem 3bitr2ri

Step	Hyp	Ref	Expression
1		3bitr2i.1	. . 3
2		3bitr2i.2	. . 3
3	1, 2	bitr4i 252	. 2
4		3bitr2i.3	. 2
5	3, 4	bitr2i 250	1

Syntax hints:  <->wb 184

This theorem is referenced by:  ssrab  3577  copsex2gb  5118  relop  5158  dmopab3  5220  issref  5385  fununi  5659  dffv2  5946  dfsup2  7922  kmlem3  8553  recmulnq  9363  ovoliunlem1  21913  shne0i  26366  ssiun3  27426  cnvoprab  27546  ind1a  28034  bnj1304  33878  bnj1253  34073  dalem20  35417  rp-isfinite6  37744

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