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

Theorem 3bitrri 299
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 277 . 2 (𝜒𝜑)
51, 4bitr3i 278 1 (𝜃𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 207
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 208
This theorem is referenced by:  nbbn  385  pm5.17  1005  dn1  1049  noranOLD  1518  2sb6rfOLD  2490  dfeumo  2612  2ex2rexrot  3247  sbralie  3469  reu8  3721  unass  4139  ssin  4204  difab  4269  csbab  4386  iunss  4960  poirr  5478  elvvv  5620  cnvuni  5750  dfco2  6091  resin  6629  dffv2  6749  dff1o6  7023  fsplit  7801  sbthcl  8627  fiint  8783  rankf  9211  dfac3  9535  dfac5lem3  9539  elznn0  11984  elnn1uz2  12313  lsmspsn  19785  cmbr2i  29300  pjss2i  29384  iuninc  30240  dffr5  32886  brsset  33247  brtxpsd  33252  ellines  33510  itg2addnclem3  34826  dvasin  34859  cvlsupr3  36360  dihglb2  38358  ifpidg  39735  dfsucon  39767  iscard4  39778  ss2iundf  39882  dffrege76  40163  dffrege99  40186  ntrneikb  40322  iunssf  41229  disjinfi  41330
  Copyright terms: Public domain W3C validator