Theorem bibi2i 226

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

Syntax hints:   <-> wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bibi1i  227  bibi12i  228  bibi2d  231  pm4.71r  387  sblbis  1931  sbrbif  1933  abeq2  2246  abid2f  2304  necon4biddc  2381  pm13.183  2817  disj3  3410  euabsn2  3587  a9evsep  4045  inex1  4057  zfpair2  4127  sucel  4327  bdinex1  13086  bj-zfpair2  13097  bj-d0clsepcl  13112