Theorem bibi1i 339

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 221	. 2 ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜒 ↔ 𝜑))
2		bibi2i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
3	2	bibi2i 338	. 2 ⊢ ((𝜒 ↔ 𝜑) ↔ (𝜒 ↔ 𝜓))
4		bicom 221	. 2 ⊢ ((𝜒 ↔ 𝜓) ↔ (𝜓 ↔ 𝜒))
5	1, 3, 4	3bitri 297	1 ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜒))

Syntax hints:   ↔ wb 205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  bibi12i  340  biluk  387  biadaniALT  820  nanass  1509  xorass  1515  hadbi  1600  hadcoma  1601  hadnot  1604  sbrbis  2307  csbied  3932  ssequn1  4181  ab0w  4374  asymref  6118  aceq1  10112  aceq0  10113  zfac  10455  zfcndac  10614  hashreprin  33663  axacprim  34707  eliminable-abeqv  35794  wl-3xorcoma  36407  wl-3xornot  36410  redundpbi1  37549  onsupmaxb  42036  rp-fakeanorass  42312  ichn  46172  dfich2  46174