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  1983  dvelimfv  1984  dvelimor  1991  dcne  2317  unass  3228  undi  3319  undif3ss  3332  symdifxor  3337  undif4  3420  iinuniss  3890  ordsucim  4411  suc11g  4467  qfto  4923  nntri3or  6382  reapcotr  8353  elnn0  8972  elxnn0  9035  elnn1uz2  9394  nn01to3  9402  elxr  9556  xaddcom  9637  xnegdi  9644  xpncan  9647  xleadd1a  9649  lcmdvds  11749  mulgcddvds  11764  cncongr2  11774  bj-peano4  13142