Theorem orbi12i 753

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

Syntax hints:   ↔ wb 104   ∨ wo 697

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 698

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  andir  808  anddi  810  3orbi123i  1171  3or6  1301  excxor  1356  19.33b2  1608  sbequilem  1810  sborv  1862  sbor  1925  r19.43  2587  rexun  3251  indi  3318  difindiss  3325  symdifxor  3337  unab  3338  dfpr2  3541  rabrsndc  3586  pwprss  3727  pwtpss  3728  unipr  3745  uniun  3750  iunun  3886  iunxun  3887  brun  3974  pwunss  4200  ordsoexmid  4472  onintexmid  4482  dcextest  4490  opthprc  4585  cnvsom  5077  ftpg  5597  tpostpos  6154  eldju  6946  djur  6947  ltexprlemloc  7408  axpre-ltwlin  7684  axpre-apti  7686  axpre-mulext  7689  axpre-suploc  7703  fz01or  9884  cbvsum  11122  fsum3  11149  cbvprod  11320  gcdsupex  11635  gcdsupcl  11636