Theorem bibi2i 460

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 396	. 2 |- ((ch <-> ph) <-> ((ch -> ph) /\ (ph -> ch)))
2		bibi.a	. . . 4 |- (ph <-> ps)
3	2	imbi1i 161	. . 3 |- ((ph -> ch) <-> (ps -> ch))
4	3	anbi2i 367	. 2 |- (((ch -> ph) /\ (ph -> ch)) <-> ((ch -> ph) /\ (ps -> ch)))
5	2	imbi2i 160	. . . 4 |- ((ch -> ph) <-> (ch -> ps))
6	5	anbi1i 368	. . 3 |- (((ch -> ph) /\ (ps -> ch)) <-> ((ch -> ps) /\ (ps -> ch)))
7		bi 396	. . 3 |- ((ch <-> ps) <-> ((ch -> ps) /\ (ps -> ch)))
8	6, 7	bitr4 154	. 2 |- (((ch -> ph) /\ (ps -> ch)) <-> (ch <-> ps))
9	1, 4, 8	3bitr 155	1 |- ((ch <-> ph) <-> (ch <-> ps))

Syntax hints:   -> wi 2   <-> wb 127   /\ wa 196

This theorem is referenced by:  bibi1i 461  bibi12i 462  pm4.71r 482  biluk 512  sblbis 891  sbrbif 893  cleqab 1174  zfrep3 1476  zfaus 1480  inex1 1697  disj3 1736  eusn 1913  sucel 2296  cleqfvf 2881

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org