Theorem orbi2i 762

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

Syntax hints:   ↔ wb 105   ∨ wo 708

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 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1i  763  orbi12i  764  orass  767  or4  771  or42  772  orordir  774  dcnnOLD  849  orbididc  953  3orcomb  987  excxor  1378  xordc  1392  nf4dc  1670  nf4r  1671  19.44  1682  dveeq2  1815  dvelimALT  2010  dvelimfv  2011  dvelimor  2018  dcne  2358  unass  3294  undi  3385  undif3ss  3398  symdifxor  3403  undif4  3487  iinuniss  3971  ordsucim  4501  suc11g  4558  qfto  5020  nntri3or  6496  reapcotr  8557  elnn0  9180  elxnn0  9243  elnn1uz2  9609  nn01to3  9619  elxr  9778  xaddcom  9863  xnegdi  9870  xpncan  9873  xleadd1a  9875  lcmdvds  12081  mulgcddvds  12096  cncongr2  12106  pythagtrip  12285  bj-peano4  14746  apdifflemr  14834