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  4310  ab0orv  4348  rexprg  4663  brsymdif  5168  nfnid  5332  asymref  6091  isocnv2  7308  zfcndrep  10573  f1omvdco3  19385  brtxpsd  35877  eliminable-abeqab  36851  bj-sbeq  36884  bj-rcleqf  37008  symrefref3  38550  eldisjn0el  38793  abbibw  42658  rp-fakeoranass  43496  rp-fakeinunass  43497  relexp0eq  43683  permaxext  44988  absnsb  47018  ichcom  47450  ichbi12i  47451