Theorem orbi2i 751

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 119	. . 3 ⊢ (𝜑 → 𝜓)
3	2	orim2i 750	. 2 ⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓))
4	1	biimpri 132	. . 3 ⊢ (𝜓 → 𝜑)
5	4	orim2i 750	. 2 ⊢ ((𝜒 ∨ 𝜓) → (𝜒 ∨ 𝜑))
6	3, 5	impbii 125	1 ⊢ ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓))

Syntax hints:   ↔ wb 104   ∨ wo 697

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orbi1i  752  orbi12i  753  orass  756  or4  760  or42  761  orordir  763  dcnnOLD  834  orbididc  937  3orcomb  971  excxor  1356  xordc  1370  nf4dc  1648  nf4r  1649  19.44  1660  dveeq2  1787  dvelimALT  1985  dvelimfv  1986  dvelimor  1993  dcne  2319  unass  3233  undi  3324  undif3ss  3337  symdifxor  3342  undif4  3425  iinuniss  3895  ordsucim  4416  suc11g  4472  qfto  4928  nntri3or  6389  reapcotr  8360  elnn0  8979  elxnn0  9042  elnn1uz2  9401  nn01to3  9409  elxr  9563  xaddcom  9644  xnegdi  9651  xpncan  9654  xleadd1a  9656  lcmdvds  11760  mulgcddvds  11775  cncongr2  11785  bj-peano4  13153