Theorem bibi1i 340

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

Syntax hints:   ↔ wb 208

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 209

This theorem is referenced by:  bibi12i  341  biluk  388  biadaniALT  830  nanass  1529  xorass  1534  hadbi  1617  hadcoma  1618  hadnot  1621  sbrbis  2342  csbied  3888  dfss2  3922  ssequn1  4138  asymref  6100  aceq1  10070  aceq0  10071  zfac  10414  zfcndac  10574  hashreprin  34878  axacprim  36021  eliminable-abeqv  37316  wl-3xorcoma  37936  wl-3xornot  37939  redundpbi1  39178  onsupmaxb  43780  rp-fakeanorass  44053  ichn  48026  dfich2  48028