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  1640  sbequilem  1849  sborv  1902  sbor  1970  r19.43  2652  rexun  3339  indi  3406  difindiss  3413  symdifxor  3425  unab  3426  dfpr2  3637  rabrsndc  3686  pwprss  3831  pwtpss  3832  unipr  3849  uniun  3854  iunun  3991  iunxun  3992  brun  4080  pwunss  4314  ordsoexmid  4594  onintexmid  4605  dcextest  4613  opthprc  4710  cnvsom  5209  ftpg  5742  tpostpos  6317  eldju  7127  djur  7128  ltexprlemloc  7667  axpre-ltwlin  7943  axpre-apti  7945  axpre-mulext  7948  axpre-suploc  7962  fz01or  10177  cbvsum  11503  fsum3  11530  cbvprod  11701  fprodseq  11726  gcdsupex  12094  gcdsupcl  12095  pythagtriplem2  12404  pythagtrip  12421