Theorem orbi12i 772

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

Syntax hints:   ↔ wb 105   ∨ wo 716

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  andir  827  anddi  829  ifptru  998  ifpfal  999  3orbi123i  1216  3or6  1360  excxor  1423  19.33b2  1678  sbequilem  1887  sborv  1941  sbor  2010  r19.43  2703  rexun  3403  indi  3472  difindiss  3479  symdifxor  3491  unab  3492  elif  3638  dfpr2  3713  rabrsndc  3764  pwprss  3915  pwtpss  3916  unipr  3933  uniun  3938  iunun  4075  iunxun  4076  brun  4166  pwunss  4409  ordsoexmid  4689  onintexmid  4700  dcextest  4708  opthprc  4806  cnvsom  5311  ftpg  5873  tpostpos  6508  eldju  7372  djur  7373  ltexprlemloc  7938  axpre-ltwlin  8214  axpre-apti  8216  axpre-mulext  8219  axpre-suploc  8233  fz01or  10467  cbvsum  12070  fsum3  12098  cbvprod  12269  fprodseq  12294  gcdsupex  12678  gcdsupcl  12679  pythagtriplem2  12989  pythagtrip  13006