Theorem bibi2i 314

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 23	. . 3 |- ( ( ch <-> ph ) -> ( ch <-> ph ) )
2		bibi2i.1	. . 3 |- ( ph <-> ps )
3	1, 2	syl6bb 264	. 2 |- ( ( ch <-> ph ) -> ( ch <-> ps ) )
4		id 23	. . 3 |- ( ( ch <-> ps ) -> ( ch <-> ps ) )
5	4, 2	syl6bbr 266	. 2 |- ( ( ch <-> ps ) -> ( ch <-> ph ) )
6	3, 5	impbii 190	1 |- ( ( ch <-> ph ) <-> ( ch <-> ps ) )

Syntax hints:   <-> wb 187

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 188

This theorem is referenced by:  bibi1i  315  bibi12i  316  bibi2d  319  con2bi  329  pm4.71r  635  xorass  1404  xorassOLD  1405  sblbis  2196  sbrbif  2198  abeq2  2544  abid2fOLD  2612  abeq2f  2613  pm13.183  3209  symdifass  3699  disj3  3834  euabsn2  4065  axrep5  4534  axsep  4538  ax6vsep  4543  inex1  4557  axpr  4651  zfpair2  4653  sucel  5506  suppvalbr  6920  bnj89  29312  bnj145OLD  29320  axrepprim  30114  brtxpsd3  30445  bisym1  30861  bj-abeq2  31136  bj-axrep5  31155  bj-axsep  31156  bj-snsetex  31303  ifpidg  35838  nanorxor  36294