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  3385  indi  3452  difindiss  3459  symdifxor  3471  unab  3472  elif  3615  dfpr2  3686  rabrsndc  3737  pwprss  3887  pwtpss  3888  unipr  3905  uniun  3910  iunun  4047  iunxun  4048  brun  4138  pwunss  4378  ordsoexmid  4658  onintexmid  4669  dcextest  4677  opthprc  4775  cnvsom  5278  ftpg  5833  tpostpos  6425  eldju  7258  djur  7259  ltexprlemloc  7817  axpre-ltwlin  8093  axpre-apti  8095  axpre-mulext  8098  axpre-suploc  8112  fz01or  10336  cbvsum  11911  fsum3  11938  cbvprod  12109  fprodseq  12134  gcdsupex  12518  gcdsupcl  12519  pythagtriplem2  12829  pythagtrip  12846