Theorem bibi1i 341

Description: Inference adding a biconditional to the right in an equivalence. (Contributed by NM, 26-May-1993.)

Hypothesis

Ref	Expression
bibi2i.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
bibi1i	⊢ ((𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜒))

Proof of Theorem bibi1i

Step	Hyp	Ref	Expression
1		bicom 225	. 2 ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜒 ↔ 𝜑))
2		bibi2i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
3	2	bibi2i 340	. 2 ⊢ ((𝜒 ↔ 𝜑) ↔ (𝜒 ↔ 𝜓))
4		bicom 225	. 2 ⊢ ((𝜒 ↔ 𝜓) ↔ (𝜓 ↔ 𝜒))
5	1, 3, 4	3bitri 300	1 ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜒))

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bibi12i  342  biluk  390  biadaniALT  833  nanass  1540  xorass  1545  hadbi  1628  hadcoma  1629  hadnot  1632  sbrbis  2343  csbied  3883  dfss2  3917  ssequn1  4132  asymref  6108  aceq1  10177  aceq0  10178  zfac  10519  zfcndac  10685  hashreprin  35232  axacprim  36441  eliminable-abeqv  37749  wl-3xorcoma  38369  wl-3xornot  38372  redundpbi1  39615  onsupmaxb  44199  rp-fakeanorass  44472  ichn  48482  dfich2  48484