Theorem orbi2i 763

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

Syntax hints:   ↔ wb 105   ∨ wo 709

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1i  764  orbi12i  765  orass  768  or4  772  or42  773  orordir  775  dcnnOLD  850  orbididc  955  3orcomb  989  excxor  1389  xordc  1403  nf4dc  1684  nf4r  1685  19.44  1696  dveeq2  1829  dvelimALT  2029  dvelimfv  2030  dvelimor  2037  dcne  2378  unass  3321  undi  3412  undif3ss  3425  symdifxor  3430  undif4  3514  iinuniss  4000  ordsucim  4537  suc11g  4594  qfto  5060  nntri3or  6560  reapcotr  8644  elnn0  9270  elxnn0  9333  elnn1uz2  9700  nn01to3  9710  elxr  9870  xaddcom  9955  xnegdi  9962  xpncan  9965  xleadd1a  9967  lcmdvds  12274  mulgcddvds  12289  cncongr2  12299  pythagtrip  12479  bj-peano4  15709  apdifflemr  15804