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  1864  dvelimALT  2064  dvelimfv  2065  dvelimor  2072  dcne  2423  unass  3376  undi  3469  undif3ss  3482  symdifxor  3487  undif4  3571  iinuniss  4074  ordsucim  4622  suc11g  4679  qfto  5152  nntri3or  6726  reapcotr  8872  elnn0  9498  elxnn0  9565  elnn1uz2  9939  nn01to3  9949  elxr  10109  xaddcom  10194  xnegdi  10201  xpncan  10204  xleadd1a  10206  lcmdvds  12776  mulgcddvds  12791  cncongr2  12801  pythagtrip  12981  bj-peano4  16725  apdifflemr  16831