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

Theorem 3bitrri 298
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 276 . 2 (𝜒𝜑)
51, 4bitr3i 277 1 (𝜃𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 206
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 207
This theorem is referenced by:  nbbn  383  pm5.17  1013  dn1  1057  sb8v  2354  sb8f  2355  dfeumo  2536  2ex2rexrot  3297  sbralie  3357  sbralieALT  3358  ceqsralt  3515  reu8  3738  sbcimdv  3858  sbcg  3862  unass  4171  ssin  4238  difab  4309  eq0rdv  4406  csbab  4439  ralidm  4511  iunssf  5043  iunss  5044  poirr  5603  elvvv  5760  cnvuni  5896  dfco2  6264  resin  6869  dffv2  7003  dff1o6  7296  fsplit  8143  naddasslem1  8733  naddasslem2  8734  sbthcl  9136  fiint  9367  fiintOLD  9368  rankf  9835  dfac3  10162  dfac5lem3  10166  elznn0  12630  elnn1uz2  12968  lsmspsn  21084  elold  27909  elzs2  28386  cmbr2i  31616  pjss2i  31700  iuninc  32574  fineqvrep  35110  dffr5  35755  brsset  35891  brtxpsd  35896  ellines  36154  itg2addnclem3  37681  dvasin  37712  cvlsupr3  39346  dihglb2  41345  oneptri  43274  faosnf0.11b  43445  ifpidg  43509  dfsucon  43541  iscard4  43551  dffrege76  43957  dffrege99  43980  ntrneikb  44112  disjinfi  45202
  Copyright terms: Public domain W3C validator