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  2347  csbied  3892  dfss2  3926  ssequn1  4142  asymref  6121  aceq1  10120  aceq0  10121  zfac  10462  zfcndac  10622  hashreprin  35039  axacprim  36220  eliminable-abeqv  37543  wl-3xorcoma  38165  wl-3xornot  38168  redundpbi1  39405  onsupmaxb  44007  rp-fakeanorass  44280  ichn  48246  dfich2  48248