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 274	1 ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜃))

Syntax hints:   ↔ wb 205

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 206

This theorem is referenced by:  pm5.32  574  biadan  817  orbidi  951  pm5.7  952  xorbi12i  1523  xorbi12iOLD  1524  norass  1538  rexbiOLD  3105  vn0  4338  ab0OLD  4375  ab0orv  4378  rexprg  4700  brsymdif  5207  nfnid  5373  asymref  6117  isocnv2  7327  zfcndrep  10608  f1omvdco3  19316  brtxpsd  34861  eliminable-abeqab  35742  bj-sbeq  35776  bj-rcleqf  35901  symrefref3  37429  eldisjn0el  37671  rp-fakeoranass  42255  rp-fakeinunass  42256  relexp0eq  42442  absnsb  45727  ichcom  46117  ichbi12i  46118