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  2459  abid2f  2515  pm13.183  2980  dfss2  3263  necompl  3545  disj3  3596  euabsn2  3792  axprimlem1  4089  axprimlem2  4090  axxpprim  4091  axsiprim  4094  axtyplowerprim  4095  axins2prim  4096  axins3prim  4097  ninexg  4098  1cex  4143  eqpw1  4163  xpkvexg  4286  p6exg  4291  eqop  4612