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 277	1 ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜃))

Syntax hints:   ↔ wb 208

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 209

This theorem is referenced by:  pm5.32  576  biadan  817  orbidi  949  pm5.7  950  xorbi12i  1515  xorbi12iOLD  1516  norass  1533  norassOLD  1534  abbiOLD  2957  brsymdif  5127  nfnid  5278  asymref  5978  isocnv2  7086  zfcndrep  10038  f1omvdco3  18579  brtxpsd  33357  bj-sbeq  34220  bj-rcleqf  34339  symrefref3  35802  rp-fakeoranass  39887  rp-fakeinunass  39888  relexp0eq  40053  absnsb  43269  ichcom  43624  ichbi12i  43625