Theorem bibi12i 315

Description: The equivalence of two equivalences. (Contributed by NM, 26-May-1993.)

Hypotheses

Ref	Expression
bibi2i.1
bibi12i.2

Assertion

Ref	Expression
bibi12i

Proof of Theorem bibi12i

Step	Hyp	Ref	Expression
1		bibi12i.2	. . 3
2	1	bibi2i 313	. 2
3		bibi2i.1	. . 3
4	3	bibi1i 314	. 2
5	2, 4	bitri 249	1

Syntax hints:  <->wb 184

This theorem is referenced by:  pm5.32  636  orbidi  932  pm5.7  934  xorbi12i  1376  abbi  2588  nfnid  4681  asymref  5388  isocnv2  6227  zfcndrep  9013  f1omvdco3  16474  brsymdif  29478  brtxpsd  29544  bj-sbeq  34468  rp-fakeoranass  37738  rp-fakeinunass  37740

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