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	|- ( ph <-> ps )

Assertion

Ref	Expression
bibi2i	|- ( ( ch <-> ph ) <-> ( ch <-> ps ) )

Proof of Theorem bibi2i

Step	Hyp	Ref	Expression
1		id 22	. . 3 |- ( ( ch <-> ph ) -> ( ch <-> ph ) )
2		bibi2i.1	. . 3 |- ( ph <-> ps )
3	1, 2	syl6bb 261	. 2 |- ( ( ch <-> ph ) -> ( ch <-> ps ) )
4		id 22	. . 3 |- ( ( ch <-> ps ) -> ( ch <-> ps ) )
5	4, 2	syl6bbr 263	. 2 |- ( ( ch <-> ps ) -> ( ch <-> ph ) )
6	3, 5	impbii 188	1 |- ( ( ch <-> ph ) <-> ( ch <-> ps ) )

Syntax hints:   <-> wb 184

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

This theorem is referenced by:  bibi1i  314  bibi12i  315  bibi2d  318  con2bi  328  pm4.71r  631  xorass  1354  sblbis  2096  sbrbif  2098  abeq2  2547  abid2f  2603  pm13.183  3099  disj3  3722  euabsn2  3945  axrep5  4407  axsep  4411  ax6vsep  4416  inex1  4432  axpr  4529  zfpair2  4531  sucel  4791  fnsnb  5897  suppvalbr  6693  legtrid  23021  abeq2f  25882  axrepprim  27352  symdifass  27857  brtxpsd3  27926  bisym1  28264  impor  28879  bnj89  31708  bnj145OLD  31716  bj-abeq2  32292  bj-axrep5  32311  bj-axsep  32312  bj-snsetex  32454