Theorem orbi2i 763

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

Syntax hints:   ↔ wb 105   ∨ wo 709

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1i  764  orbi12i  765  orass  768  or4  772  or42  773  orordir  775  dcnnOLD  850  orbididc  955  3orcomb  989  excxor  1397  xordc  1411  nf4dc  1692  nf4r  1693  19.44  1704  dveeq2  1837  dvelimALT  2037  dvelimfv  2038  dvelimor  2045  dcne  2386  unass  3329  undi  3420  undif3ss  3433  symdifxor  3438  undif4  3522  iinuniss  4009  ordsucim  4547  suc11g  4604  qfto  5071  nntri3or  6578  reapcotr  8670  elnn0  9296  elxnn0  9359  elnn1uz2  9727  nn01to3  9737  elxr  9897  xaddcom  9982  xnegdi  9989  xpncan  9992  xleadd1a  9994  lcmdvds  12343  mulgcddvds  12358  cncongr2  12368  pythagtrip  12548  bj-peano4  15824  apdifflemr  15919