Theorem orbi12i 722

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

Syntax hints:   ↔ wb 104   ∨ wo 670

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  andir  774  anddi  776  dcbii  791  3orbi123i  1139  3or6  1269  excxor  1324  19.33b2  1576  sbequilem  1777  sborv  1829  sbor  1888  r19.43  2547  rexun  3203  indi  3270  difindiss  3277  symdifxor  3289  unab  3290  dfpr2  3493  rabrsndc  3538  pwprss  3679  pwtpss  3680  unipr  3697  uniun  3702  iunun  3838  iunxun  3839  brun  3921  pwunss  4143  ordsoexmid  4415  onintexmid  4425  dcextest  4433  opthprc  4528  cnvsom  5018  ftpg  5536  tpostpos  6091  eldju  6868  djur  6869  ltexprlemloc  7316  axpre-ltwlin  7568  axpre-apti  7570  axpre-mulext  7573  fz01or  9732  cbvsum  10968  fsum3  10995  gcdsupex  11441  gcdsupcl  11442