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

Theorem 3bitrri 301
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.)
Hypotheses
Ref Expression
3bitri.1 (𝜑𝜓)
3bitri.2 (𝜓𝜒)
3bitri.3 (𝜒𝜃)
Assertion
Ref Expression
3bitrri (𝜃𝜑)

Proof of Theorem 3bitrri
StepHypRef Expression
1 3bitri.3 . 2 (𝜒𝜃)
2 3bitri.1 . . 3 (𝜑𝜓)
3 3bitri.2 . . 3 (𝜓𝜒)
42, 3bitr2i 279 . 2 (𝜒𝜑)
51, 4bitr3i 280 1 (𝜃𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 209
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 210
This theorem is referenced by:  nbbn  388  pm5.17  1009  dn1  1053  noranOLD  1528  dfeumo  2598  2ex2rexrot  3216  sbralie  3421  reu8  3675  unass  4096  ssin  4160  difab  4227  csbab  4348  iunssf  4934  iunss  4935  poirr  5453  elvvv  5595  cnvuni  5725  dfco2  6069  resin  6615  dffv2  6737  dff1o6  7014  fsplit  7799  sbthcl  8627  fiint  8783  rankf  9211  dfac3  9536  dfac5lem3  9540  elznn0  11988  elnn1uz2  12317  lsmspsn  19852  cmbr2i  29382  pjss2i  29466  iuninc  30327  dffr5  33097  brsset  33458  brtxpsd  33463  ellines  33721  itg2addnclem3  35103  dvasin  35134  cvlsupr3  36633  dihglb2  38631  ifpidg  40186  dfsucon  40218  iscard4  40228  ss2iundf  40347  dffrege76  40627  dffrege99  40650  ntrneikb  40784  disjinfi  41807
  Copyright terms: Public domain W3C validator