Theorem orbi12i 764

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

Syntax hints:   ↔ wb 105   ∨ wo 708

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 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  andir  819  anddi  821  3orbi123i  1189  3or6  1323  excxor  1378  19.33b2  1629  sbequilem  1838  sborv  1890  sbor  1954  r19.43  2635  rexun  3317  indi  3384  difindiss  3391  symdifxor  3403  unab  3404  dfpr2  3613  rabrsndc  3662  pwprss  3807  pwtpss  3808  unipr  3825  uniun  3830  iunun  3967  iunxun  3968  brun  4056  pwunss  4285  ordsoexmid  4563  onintexmid  4574  dcextest  4582  opthprc  4679  cnvsom  5174  ftpg  5702  tpostpos  6267  eldju  7069  djur  7070  ltexprlemloc  7608  axpre-ltwlin  7884  axpre-apti  7886  axpre-mulext  7889  axpre-suploc  7903  fz01or  10113  cbvsum  11370  fsum3  11397  cbvprod  11568  fprodseq  11593  gcdsupex  11960  gcdsupcl  11961  pythagtriplem2  12268  pythagtrip  12285