Theorem bibi12i 338

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 336	. 2 ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜑 ↔ 𝜃))
3		bibi2i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
4	3	bibi1i 337	. 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  572  biadan  817  orbidi  950  pm5.7  951  xorbi12i  1518  norass  1531  rexbiOLD  3095  vn0  4338  ab0OLD  4373  ab0orv  4376  rexprg  4695  brsymdif  5204  nfnid  5371  asymref  6120  isocnv2  7335  zfcndrep  10648  f1omvdco3  19443  brtxpsd  35731  eliminable-abeqab  36586  bj-sbeq  36620  bj-rcleqf  36745  symrefref3  38275  eldisjn0el  38517  abbibw  42370  rp-fakeoranass  43218  rp-fakeinunass  43219  relexp0eq  43405  absnsb  46678  ichcom  47067  ichbi12i  47068