Theorem orbi2i 757

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

Syntax hints:   ↔ wb 104   ∨ wo 703

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 704

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orbi1i  758  orbi12i  759  orass  762  or4  766  or42  767  orordir  769  dcnnOLD  844  orbididc  948  3orcomb  982  excxor  1373  xordc  1387  nf4dc  1663  nf4r  1664  19.44  1675  dveeq2  1808  dvelimALT  2003  dvelimfv  2004  dvelimor  2011  dcne  2351  unass  3284  undi  3375  undif3ss  3388  symdifxor  3393  undif4  3476  iinuniss  3953  ordsucim  4482  suc11g  4539  qfto  4998  nntri3or  6469  reapcotr  8504  elnn0  9124  elxnn0  9187  elnn1uz2  9553  nn01to3  9563  elxr  9720  xaddcom  9805  xnegdi  9812  xpncan  9815  xleadd1a  9817  lcmdvds  12020  mulgcddvds  12035  cncongr2  12045  pythagtrip  12224  bj-peano4  13912  apdifflemr  14001