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

Theorem 3bitr2ri 282
 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 260 . 2
4 3bitr2i.3 . 2
53, 4bitr2i 258 1
 Colors of variables: wff setvar class Syntax hints:   wb 189 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 190 This theorem is referenced by:  xorass  1434  ssrab  3493  copsex2gb  4950  relop  4990  dmopab3  5053  issref  5219  fununi  5659  dffv2  5953  dfsup2  7976  kmlem3  8600  recmulnq  9407  ovoliunlem1  22533  shne0i  27182  ssiun3  28251  cnvoprab  28383  ind1a  28916  bnj1304  29703  bnj1253  29898  dfrecs2  30788  icorempt2  31824  dalem20  33329  rp-isfinite6  36234  rababg  36250
 Copyright terms: Public domain W3C validator