This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bibi2i

Description: Inference adding a biconditional to the left in an equivalence. (Contributed by NM, 26-May-1993) (Proof shortened by Andrew Salmon, 7-May-2011) (Proof shortened by Wolf Lammen, 16-May-2013)

		Ref	Expression
	Hypothesis	bibi2i.1	⊢ ( 𝜑 ↔ 𝜓 )
	Assertion	bibi2i	⊢ ( ( 𝜒 ↔ 𝜑 ) ↔ ( 𝜒 ↔ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		bibi2i.1	⊢ ( 𝜑 ↔ 𝜓 )
2		id	⊢ ( ( 𝜒 ↔ 𝜑 ) → ( 𝜒 ↔ 𝜑 ) )
3	2 1	bitrdi	⊢ ( ( 𝜒 ↔ 𝜑 ) → ( 𝜒 ↔ 𝜓 ) )
4		id	⊢ ( ( 𝜒 ↔ 𝜓 ) → ( 𝜒 ↔ 𝜓 ) )
5	4 1	bitr4di	⊢ ( ( 𝜒 ↔ 𝜓 ) → ( 𝜒 ↔ 𝜑 ) )
6	3 5	impbii	⊢ ( ( 𝜒 ↔ 𝜑 ) ↔ ( 𝜒 ↔ 𝜓 ) )