Theorem bibi2i 611

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 517	. 2 |- ((ch <-> ph) <-> ((ch -> ph) /\ (ph -> ch)))
2		bibi.a	. . . 4 |- (ph <-> ps)
3	2	imbi1i 184	. . 3 |- ((ph -> ch) <-> (ps -> ch))
4	3	anbi2i 483	. 2 |- (((ch -> ph) /\ (ph -> ch)) <-> ((ch -> ph) /\ (ps -> ch)))
5	2	imbi2i 183	. . . 4 |- ((ch -> ph) <-> (ch -> ps))
6	5	anbi1i 484	. . 3 |- (((ch -> ph) /\ (ps -> ch)) <-> ((ch -> ps) /\ (ps -> ch)))
7		dfbi2 517	. . 3 |- ((ch <-> ps) <-> ((ch -> ps) /\ (ps -> ch)))
8	6, 7	bitr4i 174	. 2 |- (((ch -> ph) /\ (ps -> ch)) <-> (ch <-> ps))
9	1, 4, 8	3bitri 175	1 |- ((ch <-> ph) <-> (ch <-> ps))

Syntax hints:   -> wi 3   <-> wb 144   /\ wa 221

This theorem is referenced by:  bibi1i 612  bibi12i 613  pm4.71r 639  pm5.55 679  sblbis 1277  sbrbif 1279  abeq2 1611  disj3 2367  eusn 2507  axrep1 2768  axrep5 2772  axsep 2776  inex1 2790  axpr 2854  zfpair2 2856  sucel 3046

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 145  df-an 223

Copyright terms: Public domain