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  8821  elnn0  9447  elxnn0  9510  elnn1uz2  9884  nn01to3  9894  elxr  10054  xaddcom  10139  xnegdi  10146  xpncan  10149  xleadd1a  10151  lcmdvds  12712  mulgcddvds  12727  cncongr2  12737  pythagtrip  12917  bj-peano4  16651  apdifflemr  16759