Theorem bibi2i 320

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 269	. 2 |- ( ( ch <-> ph ) -> ( ch <-> ps ) )
4		id 22	. . 3 |- ( ( ch <-> ps ) -> ( ch <-> ps ) )
5	4, 2	syl6bbr 271	. 2 |- ( ( ch <-> ps ) -> ( ch <-> ph ) )
6	3, 5	impbii 192	1 |- ( ( ch <-> ph ) <-> ( ch <-> ps ) )

Syntax hints:   <-> wb 189

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 190

This theorem is referenced by:  bibi1i  321  bibi12i  322  bibi2d  325  con2bi  335  pm4.71r  643  xorass  1434  xorassOLD  1435  sblbis  2253  sbrbif  2255  abeq2  2580  abeq2f  2639  pm13.183  3167  symdifass  3663  disj3  3813  euabsn2  4034  axrep5  4513  axsep  4517  ax6vsep  4522  inex1  4537  axpr  4638  zfpair2  4640  sucel  5503  suppvalbr  6937  bnj89  29599  bnj145OLD  29607  axrepprim  30401  brtxpsd3  30734  bisym1  31150  bj-abeq2  31454  bj-axrep5  31473  bj-axsep  31474  bj-snsetex  31627  ifpidg  36206  nanorxor  36723