Theorem orbi12i 776

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

This proof depends on syntax axioms:   ↔ wb 105   ∨ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  andir  831  anddi  833  ifptru  1002  ifpfal  1003  3orbi123i  1220  3or6  1364  excxor  1427  19.33b2  1682  sbequilem  1891  sborv  1945  sbor  2014  r19.43  2709  rexun  3409  indi  3478  difindiss  3485  symdifxor  3497  unab  3498  elif  3652  dfpr2  3728  rabrsndc  3779  pwprss  3931  pwtpss  3932  unipr  3949  uniun  3954  iunun  4091  iunxun  4092  brun  4182  pwunss  4428  ordsoexmid  4709  onintexmid  4720  dcextest  4728  opthprc  4826  cnvsom  5331  ftpg  5899  tpostpos  6535  eldju  7409  djur  7410  ltexprlemloc  7975  axpre-ltwlin  8251  axpre-apti  8253  axpre-mulext  8256  axpre-suploc  8270  fz01or  10529  cbvsum  12145  fsum3  12173  cbvprod  12344  fprodseq  12369  gcdsupex  12753  gcdsupcl  12754  pythagtriplem2  13068  pythagtrip  13085  wexmiddc  17208