Theorem orbi12i 766

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

Syntax hints:   ↔ wb 105   ∨ wo 710

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 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  andir  821  anddi  823  3orbi123i  1192  3or6  1336  excxor  1398  19.33b2  1652  sbequilem  1861  sborv  1914  sbor  1982  r19.43  2664  rexun  3353  indi  3420  difindiss  3427  symdifxor  3439  unab  3440  dfpr2  3652  rabrsndc  3701  pwprss  3846  pwtpss  3847  unipr  3864  uniun  3869  iunun  4006  iunxun  4007  brun  4095  pwunss  4330  ordsoexmid  4610  onintexmid  4621  dcextest  4629  opthprc  4726  cnvsom  5226  ftpg  5768  tpostpos  6350  eldju  7170  djur  7171  ltexprlemloc  7720  axpre-ltwlin  7996  axpre-apti  7998  axpre-mulext  8001  axpre-suploc  8015  fz01or  10233  cbvsum  11671  fsum3  11698  cbvprod  11869  fprodseq  11894  gcdsupex  12278  gcdsupcl  12279  pythagtriplem2  12589  pythagtrip  12606