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 221	. 2 ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜒 ↔ 𝜑))
2		bibi2i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
3	2	bibi2i 337	. 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  339  biluk  385  biadaniALT  818  nanass  1503  xorass  1508  hadbi  1591  hadcoma  1592  hadnot  1595  sbrbis  2298  csbied  3924  ssequn1  4173  ab0w  4366  asymref  6108  aceq1  10109  aceq0  10110  zfac  10452  zfcndac  10611  hashreprin  34123  axacprim  35173  eliminable-abeqv  36237  wl-3xorcoma  36850  wl-3xornot  36853  redundpbi1  37995  onsupmaxb  42502  rp-fakeanorass  42778  ichn  46634  dfich2  46636