Theorem orbi12i 754

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

Syntax hints:   ↔ wb 104   ∨ wo 698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  andir  809  anddi  811  3orbi123i  1178  3or6  1312  excxor  1367  19.33b2  1616  sbequilem  1825  sborv  1877  sbor  1941  r19.43  2622  rexun  3297  indi  3364  difindiss  3371  symdifxor  3383  unab  3384  dfpr2  3589  rabrsndc  3638  pwprss  3779  pwtpss  3780  unipr  3797  uniun  3802  iunun  3938  iunxun  3939  brun  4027  pwunss  4255  ordsoexmid  4533  onintexmid  4544  dcextest  4552  opthprc  4649  cnvsom  5141  ftpg  5663  tpostpos  6223  eldju  7024  djur  7025  ltexprlemloc  7539  axpre-ltwlin  7815  axpre-apti  7817  axpre-mulext  7820  axpre-suploc  7834  fz01or  10036  cbvsum  11287  fsum3  11314  cbvprod  11485  fprodseq  11510  gcdsupex  11875  gcdsupcl  11876  pythagtriplem2  12175  pythagtrip  12192