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  3873  dfss2  3907  ssequn1  4126  asymref  6079  aceq1  10039  aceq0  10040  zfac  10382  zfcndac  10542  hashreprin  34764  axacprim  35889  eliminable-abeqv  37174  wl-3xorcoma  37794  wl-3xornot  37797  redundpbi1  39036  onsupmaxb  43667  rp-fakeanorass  43940  ichn  47916  dfich2  47918