Theorem orbi12i 716

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

Syntax hints:   ↔ wb 103   ∨ wo 664

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  andir  768  anddi  770  dcbii  785  3orbi123i  1133  3or6  1259  excxor  1314  19.33b2  1565  sbequilem  1766  sborv  1818  sbor  1876  r19.43  2525  rexun  3178  indi  3244  difindiss  3251  symdifxor  3263  unab  3264  dfpr2  3460  rabrsndc  3505  pwprss  3644  pwtpss  3645  unipr  3662  uniun  3667  iunun  3803  iunxun  3804  brun  3883  pwunss  4101  ordsoexmid  4368  onintexmid  4378  dcextest  4386  opthprc  4477  cnvsom  4961  ftpg  5465  tpostpos  6011  eldju  6738  ltexprlemloc  7145  axpre-ltwlin  7397  axpre-apti  7399  axpre-mulext  7402  fz01or  9492  cbvsum  10713  fisum  10742  gcdsupex  11042  gcdsupcl  11043