Theorem bibi12i 339

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 337	. 2 ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜑 ↔ 𝜃))
3		bibi2i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
4	3	bibi1i 338	. 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  573  biadan  815  orbidi  949  pm5.7  950  xorbi12i  1517  xorbi12iOLD  1518  norass  1535  norassOLD  1536  abbiOLD  2879  rexbiOLD  3170  vn0  4269  ab0OLD  4306  ab0orv  4309  rexprg  4629  brsymdif  5129  nfnid  5293  asymref  6010  isocnv2  7182  zfcndrep  10301  f1omvdco3  18972  brtxpsd  34123  eliminable-abeqab  34979  bj-sbeq  35013  bj-rcleqf  35142  symrefref3  36605  rp-fakeoranass  41019  rp-fakeinunass  41020  relexp0eq  41198  absnsb  44408  ichcom  44799  ichbi12i  44800