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  820  nanass  1510  xorass  1515  hadbi  1598  hadcoma  1599  hadnot  1602  sbrbis  2309  csbied  3889  dfss2  3923  ssequn1  4139  ab0w  4332  asymref  6069  aceq1  10030  aceq0  10031  zfac  10373  zfcndac  10532  hashreprin  34590  axacprim  35682  eliminable-abeqv  36843  wl-3xorcoma  37454  wl-3xornot  37457  redundpbi1  38610  onsupmaxb  43215  rp-fakeanorass  43489  ichn  47444  dfich2  47446