Theorem orbi2i 752

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

Syntax hints:   ↔ wb 104   ∨ wo 698

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 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orbi1i  753  orbi12i  754  orass  757  or4  761  or42  762  orordir  764  dcnnOLD  839  orbididc  943  3orcomb  977  excxor  1368  xordc  1382  nf4dc  1658  nf4r  1659  19.44  1670  dveeq2  1803  dvelimALT  1998  dvelimfv  1999  dvelimor  2006  dcne  2346  unass  3278  undi  3369  undif3ss  3382  symdifxor  3387  undif4  3470  iinuniss  3947  ordsucim  4476  suc11g  4533  qfto  4992  nntri3or  6457  reapcotr  8492  elnn0  9112  elxnn0  9175  elnn1uz2  9541  nn01to3  9551  elxr  9708  xaddcom  9793  xnegdi  9800  xpncan  9803  xleadd1a  9805  lcmdvds  12007  mulgcddvds  12022  cncongr2  12032  pythagtrip  12211  bj-peano4  13797  apdifflemr  13886