Theorem bibi1i 341

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

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  bibi12i  342  biluk  389  biadaniALT  832  nanass  1540  xorass  1545  hadbi  1628  hadcoma  1629  hadnot  1632  sbrbis  2344  csbied  3890  dfss2  3924  ssequn1  4140  asymref  6118  aceq1  10102  aceq0  10103  zfac  10445  zfcndac  10605  hashreprin  34988  axacprim  36180  eliminable-abeqv  37483  wl-3xorcoma  38105  wl-3xornot  38108  redundpbi1  39345  onsupmaxb  43949  rp-fakeanorass  44222  ichn  48188  dfich2  48190