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

Syntax hints:   ↔ wb 207

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 208

This theorem is referenced by:  bibi12i  340  biluk  386  biadaniALT  826  nanass  1517  xorass  1522  hadbi  1605  hadcoma  1606  hadnot  1609  sbrbis  2320  csbied  3874  dfss2  3908  ssequn1  4122  asymref  6073  aceq1  10037  aceq0  10038  zfac  10380  zfcndac  10540  hashreprin  34811  axacprim  35942  eliminable-abeqv  37227  wl-3xorcoma  37847  wl-3xornot  37850  redundpbi1  39089  onsupmaxb  43691  rp-fakeanorass  43964  ichn  47938  dfich2  47940