NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  3bitrri GIF version

Theorem 3bitrri 263
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 241 . 2 (χφ)
51, 4bitr3i 242 1 (θφ)
Colors of variables: wff setvar class
Syntax hints:  wb 176
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 177
This theorem is referenced by:  nbbn  347  pm5.17  858  dn1  932  sbralie  2848  reu8  3032  unass  3420  ssin  3477  difab  3523  iunss  4007  insklem  4304  eqpw1relk  4479  eqtfinrelk  4486  nnadjoin  4520  cnvuni  4895  dfco2  5080  resin  5307  dff1o6  5475  txpcofun  5803  releqel  5807  fnfullfunlem1  5856  ovcelem1  6171  tcfnex  6244  nclennlem1  6248  nnc3n3p1  6278  nchoicelem10  6298  nchoicelem16  6304  fnfreclem1  6317
  Copyright terms: Public domain W3C validator