Theorem bibi2i 606

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

Hypothesis

Ref	Expression
bibi.a	⊢ (φ ↔ ψ)

Assertion

Ref	Expression
bibi2i	⊢ ((χ ↔ φ) ↔ (χ ↔ ψ))

Proof of Theorem bibi2i

Step	Hyp	Ref	Expression
1		bi 513	. 2 ⊢ ((χ ↔ φ) ↔ ((χ → φ) ⋀ (φ → χ)))
2		bibi.a	. . . 4 ⊢ (φ ↔ ψ)
3	2	imbi1i 186	. . 3 ⊢ ((φ → χ) ↔ (ψ → χ))
4	3	anbi2i 479	. 2 ⊢ (((χ → φ) ⋀ (φ → χ)) ↔ ((χ → φ) ⋀ (ψ → χ)))
5	2	imbi2i 185	. . . 4 ⊢ ((χ → φ) ↔ (χ → ψ))
6	5	anbi1i 480	. . 3 ⊢ (((χ → φ) ⋀ (ψ → χ)) ↔ ((χ → ψ) ⋀ (ψ → χ)))
7		bi 513	. . 3 ⊢ ((χ ↔ ψ) ↔ ((χ → ψ) ⋀ (ψ → χ)))
8	6, 7	bitr4 176	. 2 ⊢ (((χ → φ) ⋀ (ψ → χ)) ↔ (χ ↔ ψ))
9	1, 4, 8	3bitr 177	1 ⊢ ((χ ↔ φ) ↔ (χ ↔ ψ))

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223

This theorem is referenced by:  bibi1i 607  bibi12i 608  pm4.71r 634  pm5.55 673  sblbis 1235  sbrbif 1237  abeq2 1560  disj3 2304  eusn 2436  axrep1 2684  axrep5 2688  axsep 2692  inex1 2706  axpr 2768  zfpair2 2770  sucel 3032

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