NFE Home 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
StepHypRef Expression
1 imbid.1 . . 3
21bibi2d 309 . 2
3 bicom 191 . 2
4 bicom 191 . 2
52, 3, 43bitr4g 279 1
Colors of variables: wff setvar class
Syntax hints:   wi 4   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:  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