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

Theorem 3bitrri 287
 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 265 . 2 (𝜒𝜑)
51, 4bitr3i 266 1 (𝜃𝜑)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196 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 197 This theorem is referenced by:  nbbn  372  pm5.17  950  dn1  1028  2sb6rf  2480  reu8  3435  unass  3803  ssin  3868  difab  3929  csbab  4041  iunss  4593  poirr  5075  elvvv  5212  cnvuni  5341  dfco2  5672  resin  6196  dffv2  6310  dff1o6  6571  sbthcl  8123  fiint  8278  rankf  8695  dfac3  8982  dfac5lem3  8986  elznn0  11430  elnn1uz2  11803  lsmspsn  19132  nbgrelOLD  26279  h2hlm  27965  cmbr2i  28583  pjss2i  28667  iuninc  29505  dffr5  31769  brsset  32121  brtxpsd  32126  ellines  32384  itg2addnclem3  33593  dvasin  33626  cvlsupr3  34949  dihglb2  36948  ifpidg  38153  ss2iundf  38268  dffrege76  38550  dffrege99  38573  ntrneikb  38709  iunssf  39577  disjinfi  39694
 Copyright terms: Public domain W3C validator