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

Theorem 3bitrri 289
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 267 . 2 (𝜒𝜑)
51, 4bitr3i 268 1 (𝜃𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 197
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 198
This theorem is referenced by:  nbbn  374  pm5.17  1026  dn1  1073  2sb6rf  2612  reu8  3600  unass  3969  ssin  4031  difab  4097  csbab  4206  iunss  4753  poirr  5243  elvvv  5378  cnvuni  5510  dfco2  5848  resin  6370  dffv2  6488  dff1o6  6751  sbthcl  8317  fiint  8472  rankf  8900  dfac3  9223  dfac5lem3  9227  elznn0  11654  elnn1uz2  11980  lsmspsn  19287  nbgrelOLD  26449  h2hlm  28164  cmbr2i  28782  pjss2i  28866  iuninc  29703  dffr5  31963  brsset  32315  brtxpsd  32320  ellines  32578  itg2addnclem3  33773  dvasin  33806  cvlsupr3  35122  dihglb2  37120  ifpidg  38333  ss2iundf  38448  dffrege76  38730  dffrege99  38753  ntrneikb  38889  iunssf  39753  disjinfi  39866
  Copyright terms: Public domain W3C validator