Theorem bibi2i 313

Description: Inference adding a biconditional to the left in an equivalence. (Contributed by NM, 26-May-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 16-May-2013.)

Hypothesis

Ref	Expression
bibi2i.1

Assertion

Ref	Expression
bibi2i

Proof of Theorem bibi2i

Step	Hyp	Ref	Expression
1		id 22	. . 3
2		bibi2i.1	. . 3
3	1, 2	syl6bb 261	. 2
4		id 22	. . 3
5	4, 2	syl6bbr 263	. 2
6	3, 5	impbii 188	1

Syntax hints:  <->wb 184

This theorem is referenced by:  bibi1i  314  bibi12i  315  bibi2d  318  con2bi  328  pm4.71r  631  xorass  1367  sblbis  2145  sbrbif  2147  abeq2  2581  abid2fOLD  2649  pm13.183  3240  disj3  3871  euabsn2  4101  axrep5  4568  axsep  4572  ax6vsep  4577  inex1  4593  axpr  4690  zfpair2  4692  sucel  4956  suppvalbr  6922  abeq2f  27398  axrepprim  29074  symdifass  29477  brtxpsd3  29546  bisym1  29884  nanorxor  31185  bnj89  33774  bnj145OLD  33782  bj-abeq2  34359  bj-axrep5  34378  bj-axsep  34379  bj-snsetex  34521  bj-ifidg  37707

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