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  1831  sbrbif  1833  abeq2  2143  abid2f  2199  necon4biddc  2274  pm13.183  2675  disj3  3266  euabsn2  3430  a9evsep  3870  inex1  3882  zfpair2  3936  sucel  4113  bdinex1  9354  bj-zfpair2  9365  bj-d0clsepcl  9384