Theorem bibi2i 304

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

Syntax hints:   <-> wb 176

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

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  bibi1i  305  bibi12i  306  bibi2d  309  con2bi  318  pm4.71r  612  xorass  1308  sblbis  2072  sbrbif  2074  abeq2  2458  abid2f  2514  pm13.183  2979  dfss2  3262  necompl  3544  disj3  3595  euabsn2  3791  axprimlem1  4088  axprimlem2  4089  axxpprim  4090  axsiprim  4093  axtyplowerprim  4094  axins2prim  4095  axins3prim  4096  ninexg  4097  1cex  4142  eqpw1  4162  xpkvexg  4285  p6exg  4290  eqop  4611