Theorem orbi2i 770

Description: Inference adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Dec-2012.)

Hypothesis

Ref	Expression
orbi2i.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
orbi2i	⊢ ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓))

Proof of Theorem orbi2i

Step	Hyp	Ref	Expression
1		orbi2i.1	. . . 4 ⊢ (𝜑 ↔ 𝜓)
2	1	biimpi 120	. . 3 ⊢ (𝜑 → 𝜓)
3	2	orim2i 769	. 2 ⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓))
4	1	biimpri 133	. . 3 ⊢ (𝜓 → 𝜑)
5	4	orim2i 769	. 2 ⊢ ((𝜒 ∨ 𝜓) → (𝜒 ∨ 𝜑))
6	3, 5	impbii 126	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:  orbi1i  771  orbi12i  772  orass  775  or4  779  or42  780  orordir  782  dcnnOLD  857  orbididc  962  3orcomb  1014  excxor  1423  xordc  1437  nf4dc  1718  nf4r  1719  19.44  1730  dveeq2  1863  dvelimALT  2063  dvelimfv  2064  dvelimor  2071  dcne  2414  unass  3366  undi  3457  undif3ss  3470  symdifxor  3475  undif4  3559  iinuniss  4058  ordsucim  4604  suc11g  4661  qfto  5133  nntri3or  6704  reapcotr  8837  elnn0  9463  elxnn0  9528  elnn1uz2  9902  nn01to3  9912  elxr  10072  xaddcom  10157  xnegdi  10164  xpncan  10167  xleadd1a  10169  lcmdvds  12731  mulgcddvds  12746  cncongr2  12756  pythagtrip  12936  bj-peano4  16671  apdifflemr  16779