Theorem bibi12i 340

Description: The equivalence of two equivalences. (Contributed by NM, 26-May-1993.)

Hypotheses

Ref	Expression
bibi2i.1	⊢ (𝜑 ↔ 𝜓)
bibi12i.2	⊢ (𝜒 ↔ 𝜃)

Assertion

Ref	Expression
bibi12i	⊢ ((𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜃))

Proof of Theorem bibi12i

Step	Hyp	Ref	Expression
1		bibi12i.2	. . 3 ⊢ (𝜒 ↔ 𝜃)
2	1	bibi2i 338	. 2 ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜑 ↔ 𝜃))
3		bibi2i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
4	3	bibi1i 339	. 2 ⊢ ((𝜑 ↔ 𝜃) ↔ (𝜓 ↔ 𝜃))
5	2, 4	bitri 275	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:  pm5.32  575  biadan  818  orbidi  952  pm5.7  953  xorbi12i  1524  xorbi12iOLD  1525  norass  1539  rexbiOLD  3106  vn0  4339  ab0OLD  4376  ab0orv  4379  rexprg  4701  brsymdif  5208  nfnid  5374  asymref  6118  isocnv2  7328  zfcndrep  10609  f1omvdco3  19317  brtxpsd  34897  eliminable-abeqab  35795  bj-sbeq  35829  bj-rcleqf  35954  symrefref3  37482  eldisjn0el  37724  rp-fakeoranass  42313  rp-fakeinunass  42314  relexp0eq  42500  absnsb  45785  ichcom  46175  ichbi12i  46176