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  3340  indi  3407  difindiss  3414  symdifxor  3426  unab  3427  dfpr2  3638  rabrsndc  3687  pwprss  3832  pwtpss  3833  unipr  3850  uniun  3855  iunun  3992  iunxun  3993  brun  4081  pwunss  4315  ordsoexmid  4595  onintexmid  4606  dcextest  4614  opthprc  4711  cnvsom  5210  ftpg  5743  tpostpos  6319  eldju  7129  djur  7130  ltexprlemloc  7669  axpre-ltwlin  7945  axpre-apti  7947  axpre-mulext  7950  axpre-suploc  7964  fz01or  10180  cbvsum  11506  fsum3  11533  cbvprod  11704  fprodseq  11729  gcdsupex  12097  gcdsupcl  12098  pythagtriplem2  12407  pythagtrip  12424