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

Theorem 3bitr3i 266
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 19-Aug-1993.)
Hypotheses
Ref Expression
3bitr3i.1 (φψ)
3bitr3i.2 (φχ)
3bitr3i.3 (ψθ)
Assertion
Ref Expression
3bitr3i (χθ)

Proof of Theorem 3bitr3i
StepHypRef Expression
1 3bitr3i.2 . . 3 (φχ)
2 3bitr3i.1 . . 3 (φψ)
31, 2bitr3i 242 . 2 (χψ)
4 3bitr3i.3 . 2 (ψθ)
53, 4bitri 240 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:  an12  772  cadan  1392  19.35  1600  cbval2  2004  cbvex2  2005  sbco2d  2087  equsb3  2102  elsb3  2103  elsb4  2104  sbcom2  2114  dfsb7  2119  sb7f  2120  eq2tri  2412  eqsb3  2454  clelsb3  2455  r19.35  2758  ralcom4  2877  rexcom4  2878  ceqsralt  2882  gencbvex  2901  gencbval  2903  ceqsrexbv  2973  euind  3023  reuind  3039  sbccomlem  3116  sbccom  3117  ab0  3569  difcom  3634  uniintsn  3963  pw1in  4164  dfimak2  4298  addcass  4415  elswap  4740  elxp2  4802  eqbrriv  4851  opelcnv  4893  dm0rn0  4921  opelres  4950  rninxp  5060  fununi  5160  dfoprab2  5558  opsnelsi  5774  oteltxp  5782  funsex  5828  pw1fnex  5852  brpw1fn  5854  nenpw1pwlem1  6084  lecex  6115  el2c  6191  brtcfn  6246
  Copyright terms: Public domain W3C validator