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  574  biadan  816  orbidi  950  pm5.7  951  xorbi12i  1522  xorbi12iOLD  1523  norass  1537  rexbiOLD  3105  vn0  4282  ab0OLD  4319  ab0orv  4322  rexprg  4640  brsymdif  5144  nfnid  5311  asymref  6041  isocnv2  7239  zfcndrep  10440  f1omvdco3  19124  brtxpsd  34257  eliminable-abeqab  35112  bj-sbeq  35146  bj-rcleqf  35275  symrefref3  36790  eldisjn0el  37032  rp-fakeoranass  41349  rp-fakeinunass  41350  relexp0eq  41537  absnsb  44780  ichcom  45170  ichbi12i  45171