Theorem bibi2i 216

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

Hypothesis

Ref	Expression
bibi.a	|- ( ph <-> ps )

Assertion

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

Proof of Theorem bibi2i

Step	Hyp	Ref	Expression
1		id 19	. . 3 |- ( ( ch <-> ph ) -> ( ch <-> ph ) )
2		bibi.a	. . 3 |- ( ph <-> ps )
3	1, 2	syl6bb 185	. 2 |- ( ( ch <-> ph ) -> ( ch <-> ps ) )
4		id 19	. . 3 |- ( ( ch <-> ps ) -> ( ch <-> ps ) )
5	4, 2	syl6bbr 187	. 2 |- ( ( ch <-> ps ) -> ( ch <-> ph ) )
6	3, 5	impbii 117	1 |- ( ( ch <-> ph ) <-> ( ch <-> ps ) )

Syntax hints:   <-> wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  bibi1i  217  bibi12i  218  bibi2d  221  pm4.71r  370  sblbis  1834  sbrbif  1836  abeq2  2146  abid2f  2202  necon4biddc  2280  pm13.183  2681  disj3  3272  euabsn2  3439  a9evsep  3879  inex1  3891  zfpair2  3945  sucel  4147  bdinex1  10019  bj-zfpair2  10030  bj-d0clsepcl  10049