Theorem bibi12i 343

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

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  pm5.32  577  biadan  818  orbidi  950  pm5.7  951  xorbi12i  1516  xorbi12iOLD  1517  norass  1534  norassOLD  1535  abbiOLD  2892  rexbi  3169  vn0  4237  ab0  4272  ab0orv  4275  brsymdif  5091  nfnid  5244  asymref  5948  isocnv2  7078  zfcndrep  10074  f1omvdco3  18644  brtxpsd  33745  eliminable-abeqab  34587  bj-sbeq  34622  bj-rcleqf  34742  symrefref3  36240  rp-fakeoranass  40595  rp-fakeinunass  40596  relexp0eq  40775  absnsb  43985  ichcom  44344  ichbi12i  44345