Theorem bibi12i 340

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 338	. 2 ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜑 ↔ 𝜃))
3		bibi2i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
4	3	bibi1i 339	. 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  574  biadan  816  orbidi  950  pm5.7  951  xorbi12i  1520  xorbi12iOLD  1521  norass  1535  norassOLD  1536  abbiOLD  2881  rexbiOLD  3175  vn0  4273  ab0OLD  4310  ab0orv  4313  rexprg  4633  brsymdif  5134  nfnid  5299  asymref  6026  isocnv2  7211  zfcndrep  10379  f1omvdco3  19066  brtxpsd  34205  eliminable-abeqab  35061  bj-sbeq  35095  bj-rcleqf  35224  symrefref3  36685  rp-fakeoranass  41128  rp-fakeinunass  41129  relexp0eq  41316  absnsb  44532  ichcom  44922  ichbi12i  44923