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  1553  norass  1566  rexprg  4654  brsymdif  5158  nfnid  5337  asymref  6112  isocnv2  7343  zfcndrep  10706  f1omvdco3  19672  angmgmaddcpbl  29399  brtxpsd  36752  eliminable-abeqab  37876  bj-sbeq  37909  bj-rcleqf  38034  bj-vn0ALT  38095  symrefref3  39689  eldisjn0el  39950  abbibw  43797  rp-fakeoranass  44624  rp-fakeinunass  44625  relexp0eq  44810  permaxext  46103  absnsb  48205  ichcom  48649  ichbi12i  48650