Theorem bibi12i 343

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 341	. 2 ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜑 ↔ 𝜃))
3		bibi2i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
4	3	bibi1i 342	. 2 ⊢ ((𝜑 ↔ 𝜃) ↔ (𝜓 ↔ 𝜃))
5	2, 4	bitri 278	1 ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜃))

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  pm5.32  577  biadan  818  orbidi  950  pm5.7  951  xorbi12i  1516  xorbi12iOLD  1517  norass  1534  norassOLD  1535  abbiOLD  2930  brsymdif  5089  nfnid  5241  asymref  5943  isocnv2  7063  zfcndrep  10025  f1omvdco3  18569  brtxpsd  33468  eliminable-abeqab  34306  bj-sbeq  34342  bj-rcleqf  34461  symrefref3  35960  rp-fakeoranass  40222  rp-fakeinunass  40223  relexp0eq  40402  absnsb  43619  ichcom  43976  ichbi12i  43977