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  835  orbididc  938  3orcomb  972  excxor  1357  xordc  1371  nf4dc  1649  nf4r  1650  19.44  1661  dveeq2  1788  dvelimALT  1986  dvelimfv  1987  dvelimor  1994  dcne  2320  unass  3238  undi  3329  undif3ss  3342  symdifxor  3347  undif4  3430  iinuniss  3903  ordsucim  4424  suc11g  4480  qfto  4936  nntri3or  6397  reapcotr  8384  elnn0  9003  elxnn0  9066  elnn1uz2  9428  nn01to3  9436  elxr  9593  xaddcom  9674  xnegdi  9681  xpncan  9684  xleadd1a  9686  lcmdvds  11796  mulgcddvds  11811  cncongr2  11821  bj-peano4  13324  apdifflemr  13415