Theorem bibi2i 608

Description: Inference adding a biconditional to the left in an equivalence.

Hypothesis

Ref	Expression
bibi.a	|- (ph <-> ps)

Assertion

Ref	Expression
bibi2i	|- ((ch <-> ph) <-> (ch <-> ps))

Proof of Theorem bibi2i

Step	Hyp	Ref	Expression
1		dfbi2 514	. 2 |- ((ch <-> ph) <-> ((ch -> ph) /\ (ph -> ch)))
2		bibi.a	. . . 4 |- (ph <-> ps)
3	2	imbi1i 186	. . 3 |- ((ph -> ch) <-> (ps -> ch))
4	3	anbi2i 480	. 2 |- (((ch -> ph) /\ (ph -> ch)) <-> ((ch -> ph) /\ (ps -> ch)))
5	2	imbi2i 185	. . . 4 |- ((ch -> ph) <-> (ch -> ps))
6	5	anbi1i 481	. . 3 |- (((ch -> ph) /\ (ps -> ch)) <-> ((ch -> ps) /\ (ps -> ch)))
7		dfbi2 514	. . 3 |- ((ch <-> ps) <-> ((ch -> ps) /\ (ps -> ch)))
8	6, 7	bitr4 176	. 2 |- (((ch -> ph) /\ (ps -> ch)) <-> (ch <-> ps))
9	1, 4, 8	3bitr 177	1 |- ((ch <-> ph) <-> (ch <-> ps))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223

This theorem is referenced by:  bibi1i 609  bibi12i 610  pm4.71r 636  pm5.55 675  sblbis 1240  sbrbif 1242  abeq2 1568  disj3 2314  eusn 2446  axrep1 2694  axrep5 2698  axsep 2702  inex1 2716  axpr 2778  zfpair2 2780  sucel 3042

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

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain