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

Theorem 3bitrri 286
 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 264 . 2 (𝜒𝜑)
51, 4bitr3i 265 1 (𝜃𝜑)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195 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 196 This theorem is referenced by:  nbbn  372  pm5.17  928  dn1  1000  2sb6rf  2440  reu8  3369  unass  3732  ssin  3797  difab  3855  csbab  3960  iunss  4497  poirr  4970  elvvv  5101  cnvuni  5231  dfco2  5551  resin  6071  dffv2  6181  dff1o6  6431  sbthcl  7967  fiint  8122  rankf  8540  dfac3  8827  dfac5lem3  8831  elznn0  11269  elnn1uz2  11641  lsmspsn  18905  usg2spot2nb  26592  h2hlm  27221  cmbr2i  27839  pjss2i  27923  iuninc  28761  dffr5  30896  brsset  31166  brtxpsd  31171  ellines  31429  itg2addnclem3  32633  dvasin  32666  cvlsupr3  33649  dihglb2  35649  ifpidg  36855  ss2iundf  36970  dffrege76  37253  dffrege99  37276  ntrneikb  37412  iunssf  38290  disjinfi  38375  nbgrel  40564
 Copyright terms: Public domain W3C validator