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  4311  ab0orv  4349  rexprg  4664  brsymdif  5169  nfnid  5333  asymref  6092  isocnv2  7309  zfcndrep  10574  f1omvdco3  19386  brtxpsd  35889  eliminable-abeqab  36863  bj-sbeq  36896  bj-rcleqf  37020  symrefref3  38562  eldisjn0el  38805  abbibw  42672  rp-fakeoranass  43510  rp-fakeinunass  43511  relexp0eq  43697  permaxext  45002  absnsb  47032  ichcom  47464  ichbi12i  47465