Theorem bibi12i 342

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

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  pm5.32  584  biadan  831  orbidi  967  pm5.7  968  xorbi12i  1554  norass  1567  abbib  2832  rexprg  4659  brsymdif  5165  nfnid  5344  asymref  6128  isocnv2  7370  zfcndrep  10738  f1omvdco3  19714  angmgmaddcpbl  29447  brtxpsd  36871  eliminable-abeqab  37995  bj-sbeq  38028  bj-rcleqf  38153  bj-vn0ALT  38257  symrefref3  39846  eldisjn0el  40107  abbibw  43954  rp-fakeoranass  44776  rp-fakeinunass  44777  relexp0eq  44962  permaxext  46259  absnsb  48370  ichcom  48814  ichbi12i  48815