Theorem bibi2i 315

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

Syntax hints:   <-> wb 188

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 189

This theorem is referenced by:  bibi1i  316  bibi12i  317  bibi2d  320  con2bi  330  pm4.71r  637  xorass  1409  xorassOLD  1410  sblbis  2233  sbrbif  2235  abeq2  2560  abeq2f  2619  pm13.183  3179  symdifass  3672  disj3  3809  euabsn2  4043  axrep5  4520  axsep  4524  ax6vsep  4529  inex1  4544  axpr  4638  zfpair2  4640  sucel  5496  suppvalbr  6918  bnj89  29527  bnj145OLD  29535  axrepprim  30329  brtxpsd3  30663  bisym1  31079  bj-abeq2  31388  bj-axrep5  31407  bj-axsep  31408  bj-snsetex  31557  ifpidg  36135  nanorxor  36653