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  2346  csbied  3887  dfss2  4097  ssequn1  4187  asymref  6123  aceq1  10226  aceq0  10227  zfac  10568  zfcndac  10734  hashreprin  35332  axacprim  36663  eliminable-abeqv  37970  wl-3xorcoma  38606  wl-3xornot  38609  redundpbi1  39850  onsupmaxb  44444  rp-fakeanorass  44717  ichn  48753  dfich2  48755