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  2344  csbied  3886  dfss2  3920  ssequn1  4135  asymref  6114  aceq1  10124  aceq0  10125  zfac  10466  zfcndac  10632  hashreprin  35136  axacprim  36294  eliminable-abeqv  37618  wl-3xorcoma  38240  wl-3xornot  38243  redundpbi1  39471  onsupmaxb  44088  rp-fakeanorass  44361  ichn  48364  dfich2  48366