Theorem orbi12i 776

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

Syntax hints:   ↔ wb 105   ∨ wo 720

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 721

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  andir  831  anddi  833  ifptru  1002  ifpfal  1003  3orbi123i  1220  3or6  1364  excxor  1427  19.33b2  1682  sbequilem  1891  sborv  1945  sbor  2014  r19.43  2709  rexun  3409  indi  3478  difindiss  3485  symdifxor  3497  unab  3498  elif  3649  dfpr2  3724  rabrsndc  3775  pwprss  3926  pwtpss  3927  unipr  3944  uniun  3949  iunun  4086  iunxun  4087  brun  4177  pwunss  4423  ordsoexmid  4704  onintexmid  4715  dcextest  4723  opthprc  4821  cnvsom  5326  ftpg  5890  tpostpos  6525  eldju  7398  djur  7399  ltexprlemloc  7964  axpre-ltwlin  8240  axpre-apti  8242  axpre-mulext  8245  axpre-suploc  8259  fz01or  10496  cbvsum  12104  fsum3  12132  cbvprod  12303  fprodseq  12328  gcdsupex  12712  gcdsupcl  12713  pythagtriplem2  13023  pythagtrip  13040