Theorem bibi2i 305

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 20	. . 3 |- ( ( ch <-> ph ) -> ( ch <-> ph ) )
2		bibi.a	. . 3 |- ( ph <-> ps )
3	1, 2	syl6bb 253	. 2 |- ( ( ch <-> ph ) -> ( ch <-> ps ) )
4		id 20	. . 3 |- ( ( ch <-> ps ) -> ( ch <-> ps ) )
5	4, 2	syl6bbr 255	. 2 |- ( ( ch <-> ps ) -> ( ch <-> ph ) )
6	3, 5	impbii 181	1 |- ( ( ch <-> ph ) <-> ( ch <-> ps ) )

Syntax hints:   <-> wb 177

This theorem is referenced by:  bibi1i  306  bibi12i  307  bibi2d  310  con2bi  319  pm4.71r  613  xorass  1314  sblbis  2121  sbrbif  2123  abeq2  2509  abid2f  2565  pm13.183  3036  disj3  3632  euabsn2  3835  axrep5  4285  axsep  4289  ax9vsep  4294  inex1  4304  axpr  4362  zfpair2  4364  sucel  4614  abeq2f  23913  axrepprim  25104  symdifass  25585  brtxpsd3  25650  bisym1  26073  bnj89  28792  bnj145  28800  sblbisNEW7  29342  sbrbifNEW7  29344

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178