Theorem bibi1i 314

Description: Inference adding a biconditional to the right in an equivalence. (Contributed by NM, 26-May-1993.)

Hypothesis

Ref	Expression
bibi2i.1

Assertion

Ref	Expression
bibi1i

Proof of Theorem bibi1i

Step	Hyp	Ref	Expression
1		bicom 200	. 2
2		bibi2i.1	. . 3
3	2	bibi2i 313	. 2
4		bicom 200	. 2
5	1, 3, 4	3bitri 271	1

Syntax hints:  <->wb 184

This theorem is referenced by:  bibi12i  315  biluk  933  xorass  1367  hadbi  1454  sbrbis  2146  ssequn1  3673  asymref  5388  aceq1  8519  aceq0  8520  zfac  8861  zfcndac  9018  funcnvmptOLD  27509  axacprim  29079  symdifass  29477  rp-fakeanorass  37737  rp-fakenanass  37739

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 185