Theorem bibi1i 338

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

Syntax hints:   ↔ wb 206

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 207

This theorem is referenced by:  bibi12i  339  biluk  385  biadaniALT  821  nanass  1512  xorass  1517  hadbi  1600  hadcoma  1601  hadnot  1604  sbrbis  2316  csbied  3887  dfss2  3921  ssequn1  4140  asymref  6083  aceq1  10041  aceq0  10042  zfac  10384  zfcndac  10544  hashreprin  34804  axacprim  35929  eliminable-abeqv  37142  wl-3xorcoma  37760  wl-3xornot  37763  redundpbi1  38995  onsupmaxb  43625  rp-fakeanorass  43898  ichn  47845  dfich2  47847