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  1507  xorass  1512  hadbi  1595  hadcoma  1596  hadnot  1599  sbrbis  2309  csbied  3946  dfss2  3981  ssequn1  4196  ab0w  4385  asymref  6139  aceq1  10155  aceq0  10156  zfac  10498  zfcndac  10657  hashreprin  34614  axacprim  35687  eliminable-abeqv  36850  wl-3xorcoma  37461  wl-3xornot  37464  redundpbi1  38613  onsupmaxb  43228  rp-fakeanorass  43503  ichn  47381  dfich2  47383