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

---

Theorem bibi1d 310

Description: Deduction adding a biconditional to the right in an equivalence. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
imbid.1

Assertion

Ref	Expression
bibi1d

---

Proof of Theorem bibi1d

Step	Hyp	Ref	Expression
1		imbid.1	. . 3
2	1	bibi2d 309	. 2
3		bicom 191	. 2
4		bicom 191	. 2
5	2, 3, 4	3bitr4g 279	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:  bibi12d  312  bibi1  317  biass  348  eubid  2211  axext3  2336  bm1.1  2338  eqeq1  2359  pm13.183  2979  elabgt  2982  mob  3018  sbctt  3108  sbcabel  3123  br1stg  4730  isoeq2  5483  extd  5923

Copyright terms: Public domain

W3C validator