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  819  orbidi  954  pm5.7  955  xorbi12i  1521  norass  1534  rexbiOLD  3103  vn0  4351  ab0orv  4389  rexprg  4702  brsymdif  5207  nfnid  5381  asymref  6139  isocnv2  7351  zfcndrep  10652  f1omvdco3  19482  brtxpsd  35876  eliminable-abeqab  36851  bj-sbeq  36884  bj-rcleqf  37008  symrefref3  38546  eldisjn0el  38788  abbibw  42664  rp-fakeoranass  43504  rp-fakeinunass  43505  relexp0eq  43691  absnsb  46977  ichcom  47384  ichbi12i  47385