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  7408  djur  7409  ltexprlemloc  7974  axpre-ltwlin  8250  axpre-apti  8252  axpre-mulext  8255  axpre-suploc  8269  fz01or  10518  cbvsum  12126  fsum3  12154  cbvprod  12325  fprodseq  12350  gcdsupex  12734  gcdsupcl  12735  pythagtriplem2  13045  pythagtrip  13062  wexmiddc  17042