Theorem orbi12i 765

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

Syntax hints:   ↔ wb 105   ∨ wo 709

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  andir  820  anddi  822  3orbi123i  1191  3or6  1334  excxor  1389  19.33b2  1640  sbequilem  1849  sborv  1902  sbor  1966  r19.43  2648  rexun  3330  indi  3397  difindiss  3404  symdifxor  3416  unab  3417  dfpr2  3626  rabrsndc  3675  pwprss  3820  pwtpss  3821  unipr  3838  uniun  3843  iunun  3980  iunxun  3981  brun  4069  pwunss  4298  ordsoexmid  4576  onintexmid  4587  dcextest  4595  opthprc  4692  cnvsom  5187  ftpg  5717  tpostpos  6284  eldju  7092  djur  7093  ltexprlemloc  7631  axpre-ltwlin  7907  axpre-apti  7909  axpre-mulext  7912  axpre-suploc  7926  fz01or  10136  cbvsum  11395  fsum3  11422  cbvprod  11593  fprodseq  11618  gcdsupex  11985  gcdsupcl  11986  pythagtriplem2  12293  pythagtrip  12310