Theorem bibi2i 606

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		bi 513	. 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 479	. 2 |- (((ch -> ph) /\ (ph -> ch)) <-> ((ch -> ph) /\ (ps -> ch)))
5	2	imbi2i 185	. . . 4 |- ((ch -> ph) <-> (ch -> ps))
6	5	anbi1i 480	. . 3 |- (((ch -> ph) /\ (ps -> ch)) <-> ((ch -> ps) /\ (ps -> ch)))
7		bi 513	. . 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 607  bibi12i 608  pm4.71r 634  pm5.55 672  sblbis 1224  sbrbif 1226  abeq2 1544  disj3 2285  eusn 2416  axrep1 2662  axrep5 2666  axsep 2670  inex1 2684  axpr 2746  zfpair2 2748  sucel 3005

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