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

Syntax hints:   ↔ wb 206

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 207

This theorem is referenced by:  pm5.32  573  biadan  819  orbidi  955  pm5.7  956  xorbi12i  1524  norass  1537  rexbiOLD  3105  vn0  4345  ab0orv  4383  rexprg  4697  brsymdif  5202  nfnid  5375  asymref  6136  isocnv2  7351  zfcndrep  10654  f1omvdco3  19467  brtxpsd  35895  eliminable-abeqab  36869  bj-sbeq  36902  bj-rcleqf  37026  symrefref3  38565  eldisjn0el  38807  abbibw  42687  rp-fakeoranass  43527  rp-fakeinunass  43528  relexp0eq  43714  absnsb  47039  ichcom  47446  ichbi12i  47447