Theorem orbi2i 720

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

Syntax hints:   ↔ wb 104   ∨ wo 670

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orbi1i  721  orbi12i  722  orass  725  or4  729  or42  730  orordir  732  testbitestn  867  orbididc  905  3orcomb  939  excxor  1324  xordc  1338  nf4dc  1616  nf4r  1617  19.44  1628  dveeq2  1754  dvelimALT  1946  dvelimfv  1947  dvelimor  1954  dcne  2278  unass  3180  undi  3271  undif3ss  3284  symdifxor  3289  undif4  3372  iinuniss  3841  ordsucim  4354  suc11g  4410  qfto  4864  nntri3or  6319  reapcotr  8226  elnn0  8831  elxnn0  8894  elnn1uz2  9251  nn01to3  9259  elxr  9404  xaddcom  9485  xnegdi  9492  xpncan  9495  xleadd1a  9497  lcmdvds  11553  mulgcddvds  11568  cncongr2  11578  bj-peano4  12738