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  4298  ab0orv  4336  rexprg  4651  brsymdif  5154  nfnid  5317  asymref  6069  isocnv2  7272  zfcndrep  10527  f1omvdco3  19347  brtxpsd  35887  eliminable-abeqab  36861  bj-sbeq  36894  bj-rcleqf  37018  symrefref3  38560  eldisjn0el  38803  abbibw  42670  rp-fakeoranass  43507  rp-fakeinunass  43508  relexp0eq  43694  permaxext  44999  absnsb  47031  ichcom  47463  ichbi12i  47464