Theorem bibi12i 340

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 338	. 2 ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜑 ↔ 𝜃))
3		bibi2i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
4	3	bibi1i 339	. 2 ⊢ ((𝜑 ↔ 𝜃) ↔ (𝜓 ↔ 𝜃))
5	2, 4	bitri 275	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  575  biadan  818  orbidi  952  pm5.7  953  xorbi12i  1524  xorbi12iOLD  1525  norass  1539  rexbiOLD  3106  vn0  4339  ab0OLD  4376  ab0orv  4379  rexprg  4701  brsymdif  5208  nfnid  5374  asymref  6118  isocnv2  7328  zfcndrep  10609  f1omvdco3  19317  brtxpsd  34866  eliminable-abeqab  35747  bj-sbeq  35781  bj-rcleqf  35906  symrefref3  37434  eldisjn0el  37676  rp-fakeoranass  42265  rp-fakeinunass  42266  relexp0eq  42452  absnsb  45737  ichcom  46127  ichbi12i  46128