Theorem orbi12i 764

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

Syntax hints:   ↔ wb 105   ∨ wo 708

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 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  andir  819  anddi  821  3orbi123i  1189  3or6  1323  excxor  1378  19.33b2  1627  sbequilem  1836  sborv  1888  sbor  1952  r19.43  2633  rexun  3313  indi  3380  difindiss  3387  symdifxor  3399  unab  3400  dfpr2  3608  rabrsndc  3657  pwprss  3801  pwtpss  3802  unipr  3819  uniun  3824  iunun  3960  iunxun  3961  brun  4049  pwunss  4277  ordsoexmid  4555  onintexmid  4566  dcextest  4574  opthprc  4671  cnvsom  5164  ftpg  5692  tpostpos  6255  eldju  7057  djur  7058  ltexprlemloc  7581  axpre-ltwlin  7857  axpre-apti  7859  axpre-mulext  7862  axpre-suploc  7876  fz01or  10081  cbvsum  11336  fsum3  11363  cbvprod  11534  fprodseq  11559  gcdsupex  11925  gcdsupcl  11926  pythagtriplem2  12233  pythagtrip  12250