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

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
StepHypRef Expression
1 3bitr2i.1 . . 3
2 3bitr2i.2 . . 3
31, 2bitr4i 252 . 2
4 3bitr2i.3 . 2
53, 4bitr2i 250 1
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator