Theorem orbi12i 769

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 767	. 2 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜑 ∨ 𝜃))
3		orbi12i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
4	3	orbi1i 768	. 2 ⊢ ((𝜑 ∨ 𝜃) ↔ (𝜓 ∨ 𝜃))
5	2, 4	bitri 184	1 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃))

Syntax hints:   ↔ wb 105   ∨ wo 713

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  andir  824  anddi  826  ifptru  995  ifpfal  996  3orbi123i  1213  3or6  1357  excxor  1420  19.33b2  1675  sbequilem  1884  sborv  1937  sbor  2005  r19.43  2689  rexun  3384  indi  3451  difindiss  3458  symdifxor  3470  unab  3471  elif  3614  dfpr2  3685  rabrsndc  3734  pwprss  3883  pwtpss  3884  unipr  3901  uniun  3906  iunun  4043  iunxun  4044  brun  4134  pwunss  4373  ordsoexmid  4653  onintexmid  4664  dcextest  4672  opthprc  4769  cnvsom  5271  ftpg  5822  tpostpos  6408  eldju  7231  djur  7232  ltexprlemloc  7790  axpre-ltwlin  8066  axpre-apti  8068  axpre-mulext  8071  axpre-suploc  8085  fz01or  10303  cbvsum  11866  fsum3  11893  cbvprod  12064  fprodseq  12089  gcdsupex  12473  gcdsupcl  12474  pythagtriplem2  12784  pythagtrip  12801