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  818  nanass  1505  xorass  1511  hadbi  1599  hadcoma  1600  hadnot  1604  sbrbis  2307  csbied  3870  ssequn1  4114  ab0w  4307  asymref  6021  aceq1  9873  aceq0  9874  zfac  10216  zfcndac  10375  hashreprin  32600  axacprim  33648  eliminable-abeqv  35051  wl-3xorcoma  35649  wl-3xornot  35652  redundpbi1  36744  rp-fakeanorass  41120  ichn  44908  dfich2  44910