Theorem orbi2i 767

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

Syntax hints:   ↔ wb 105   ∨ wo 713

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1i  768  orbi12i  769  orass  772  or4  776  or42  777  orordir  779  dcnnOLD  854  orbididc  959  3orcomb  1011  excxor  1420  xordc  1434  nf4dc  1716  nf4r  1717  19.44  1728  dveeq2  1861  dvelimALT  2061  dvelimfv  2062  dvelimor  2069  dcne  2411  unass  3362  undi  3453  undif3ss  3466  symdifxor  3471  undif4  3555  iinuniss  4051  ordsucim  4596  suc11g  4653  qfto  5124  nntri3or  6656  reapcotr  8768  elnn0  9394  elxnn0  9457  elnn1uz2  9831  nn01to3  9841  elxr  10001  xaddcom  10086  xnegdi  10093  xpncan  10096  xleadd1a  10098  lcmdvds  12641  mulgcddvds  12656  cncongr2  12666  pythagtrip  12846  bj-peano4  16486  apdifflemr  16587