Theorem bibi12i 339

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 337	. 2 ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜑 ↔ 𝜃))
3		bibi2i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
4	3	bibi1i 338	. 2 ⊢ ((𝜑 ↔ 𝜃) ↔ (𝜓 ↔ 𝜃))
5	2, 4	bitri 275	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:  pm5.32  573  biadan  818  orbidi  954  pm5.7  955  xorbi12i  1524  norass  1537  vn0  4308  ab0orv  4346  rexprg  4661  brsymdif  5166  nfnid  5330  asymref  6089  isocnv2  7306  zfcndrep  10567  f1omvdco3  19379  brtxpsd  35882  eliminable-abeqab  36856  bj-sbeq  36889  bj-rcleqf  37013  symrefref3  38555  eldisjn0el  38798  abbibw  42665  rp-fakeoranass  43503  rp-fakeinunass  43504  relexp0eq  43690  permaxext  44995  absnsb  47028  ichcom  47460  ichbi12i  47461