Theorem orbi12i 765

Description: Infer the disjunction of two equivalences. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
orbi12i.1	⊢ (𝜑 ↔ 𝜓)
orbi12i.2	⊢ (𝜒 ↔ 𝜃)

Assertion

Ref	Expression
orbi12i	⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃))

Proof of Theorem orbi12i

Step	Hyp	Ref	Expression
1		orbi12i.2	. . 3 ⊢ (𝜒 ↔ 𝜃)
2	1	orbi2i 763	. 2 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜑 ∨ 𝜃))
3		orbi12i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
4	3	orbi1i 764	. 2 ⊢ ((𝜑 ∨ 𝜃) ↔ (𝜓 ∨ 𝜃))
5	2, 4	bitri 184	1 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃))

Syntax hints:   ↔ wb 105   ∨ wo 709

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  andir  820  anddi  822  3orbi123i  1191  3or6  1334  excxor  1389  19.33b2  1643  sbequilem  1852  sborv  1905  sbor  1973  r19.43  2655  rexun  3344  indi  3411  difindiss  3418  symdifxor  3430  unab  3431  dfpr2  3642  rabrsndc  3691  pwprss  3836  pwtpss  3837  unipr  3854  uniun  3859  iunun  3996  iunxun  3997  brun  4085  pwunss  4319  ordsoexmid  4599  onintexmid  4610  dcextest  4618  opthprc  4715  cnvsom  5214  ftpg  5749  tpostpos  6331  eldju  7143  djur  7144  ltexprlemloc  7693  axpre-ltwlin  7969  axpre-apti  7971  axpre-mulext  7974  axpre-suploc  7988  fz01or  10205  cbvsum  11544  fsum3  11571  cbvprod  11742  fprodseq  11767  gcdsupex  12151  gcdsupcl  12152  pythagtriplem2  12462  pythagtrip  12479