Theorem orbi2i 774

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

This proof depends on syntax axioms:   ↔ wb 105   ∨ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  orbi1i  775  orbi12i  776  orass  779  or4  783  or42  784  orordir  786  dcnnOLD  861  orbididc  966  3orcomb  1018  excxor  1427  xordc  1441  nf4dc  1722  nf4r  1723  19.44  1734  dveeq2  1868  dvelimALT  2070  dvelimfv  2071  dvelimor  2078  dcne  2431  unass  3386  undi  3479  undif3ss  3492  symdifxor  3497  undif4  3587  iinuniss  4095  ordsucim  4647  suc11g  4704  qfto  5177  nntri3or  6766  reapcotr  8926  elnn0  9565  elxnn0  9632  elnn1uz2  10007  nn01to3  10017  elxr  10178  xaddcom  10263  xnegdi  10270  xpncan  10273  xleadd1a  10275  hashf1lem2  11286  lcmdvds  12857  mulgcddvds  12872  cncongr2  12882  pythagtrip  13062  bj-peano4  16981  apdifflemr  17096