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  953  pm5.7  954  xorbi12i  1521  norass  1534  rexbiOLD  3111  vn0  4368  ab0OLD  4403  ab0orv  4406  rexprg  4721  brsymdif  5225  nfnid  5393  asymref  6148  isocnv2  7367  zfcndrep  10683  f1omvdco3  19491  brtxpsd  35858  eliminable-abeqab  36834  bj-sbeq  36867  bj-rcleqf  36991  symrefref3  38520  eldisjn0el  38762  abbibw  42632  rp-fakeoranass  43476  rp-fakeinunass  43477  relexp0eq  43663  absnsb  46942  ichcom  47333  ichbi12i  47334