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