Theorem orbi12i 769

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

Syntax hints:   ↔ wb 105   ∨ wo 713

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  andir  824  anddi  826  ifptru  995  ifpfal  996  3orbi123i  1213  3or6  1357  excxor  1420  19.33b2  1675  sbequilem  1884  sborv  1937  sbor  2005  r19.43  2689  rexun  3384  indi  3451  difindiss  3458  symdifxor  3470  unab  3471  elif  3614  dfpr2  3685  rabrsndc  3734  pwprss  3884  pwtpss  3885  unipr  3902  uniun  3907  iunun  4044  iunxun  4045  brun  4135  pwunss  4374  ordsoexmid  4654  onintexmid  4665  dcextest  4673  opthprc  4770  cnvsom  5272  ftpg  5827  tpostpos  6416  eldju  7246  djur  7247  ltexprlemloc  7805  axpre-ltwlin  8081  axpre-apti  8083  axpre-mulext  8086  axpre-suploc  8100  fz01or  10319  cbvsum  11886  fsum3  11913  cbvprod  12084  fprodseq  12109  gcdsupex  12493  gcdsupcl  12494  pythagtriplem2  12804  pythagtrip  12821