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  33632  axacprim  34676  eliminable-abeqv  35746  wl-3xorcoma  36359  wl-3xornot  36362  redundpbi1  37501  onsupmaxb  41988  rp-fakeanorass  42264  ichn  46124  dfich2  46126