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  1012  dn1  1058  noranOLD  1533  dfeumo  2538  2ex2rexrot  3181  sbralie  3396  reu8  3663  sbcimdv  3786  sbcg  3791  unass  4097  ssin  4162  difab  4232  eq0rdv  4336  csbab  4369  ralidm  4440  iunssf  4970  iunss  4971  poirr  5498  elvvv  5642  cnvuni  5773  dfco2  6127  resin  6704  dffv2  6828  dff1o6  7108  fsplit  7907  sbthcl  8794  fiint  8978  rankf  9440  dfac3  9765  dfac5lem3  9769  elznn0  12221  elnn1uz2  12551  lsmspsn  20154  cmbr2i  29709  pjss2i  29793  iuninc  30651  fineqvrep  32808  dffr5  33471  elold  33824  brsset  33962  brtxpsd  33967  ellines  34225  itg2addnclem3  35604  dvasin  35635  cvlsupr3  37132  dihglb2  39130  ifpidg  40831  dfsucon  40863  iscard4  40873  ss2iundf  40992  dffrege76  41272  dffrege99  41295  ntrneikb  41429  disjinfi  42452
  Copyright terms: Public domain W3C validator