Theorem bibi2i 225

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 194	. 2 |- ( ( ch <-> ph ) -> ( ch <-> ps ) )
4		id 19	. . 3 |- ( ( ch <-> ps ) -> ( ch <-> ps ) )
5	4, 2	syl6bbr 196	. 2 |- ( ( ch <-> ps ) -> ( ch <-> ph ) )
6	3, 5	impbii 124	1 |- ( ( ch <-> ph ) <-> ( ch <-> ps ) )

Syntax hints:   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  bibi1i  226  bibi12i  227  bibi2d  230  pm4.71r  382  sblbis  1875  sbrbif  1877  abeq2  2187  abid2f  2243  necon4biddc  2320  pm13.183  2732  disj3  3296  euabsn2  3461  a9evsep  3900  inex1  3912  zfpair2  3965  sucel  4165  bdinex1  10690  bj-zfpair2  10701  bj-d0clsepcl  10720