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

---

Theorem 3bitr4d 276

Description: Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 18-Oct-1995.)

Hypotheses

Ref	Expression
3bitr4d.1
3bitr4d.2
3bitr4d.3

Assertion

Ref	Expression
3bitr4d

---

Proof of Theorem 3bitr4d

Step	Hyp	Ref	Expression
1		3bitr4d.2	. 2
2		3bitr4d.1	. . 3
3		3bitr4d.3	. . 3
4	2, 3	bitr4d 247	. 2
5	1, 4	bitrd 244	1

Colors of variables: wff setvar class

Syntax hints:   wi 4   wb 176

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  sbcom  2089  sbcom2  2114  r19.12sn  3789  lefinlteq  4463  eqtfinrelk  4486  tfinlefin  4502  opbrop  4841  fvopab3g  5386  unpreima  5408  inpreima  5409  respreima  5410  fconst5  5455  isotr  5495  ncseqnc  6128

Copyright terms: Public domain

W3C validator