Theorem orbi2i 711

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

Syntax hints:   ↔ wb 103   ∨ wo 661

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  orbi1i  712  orbi12i  713  orass  716  or4  720  or42  721  orordir  723  testbitestn  856  orbididc  894  3orcomb  928  excxor  1309  xordc  1323  nf4dc  1600  nf4r  1601  19.44  1612  dveeq2  1736  dvelimALT  1927  dvelimfv  1928  dvelimor  1935  dcne  2256  unass  3129  undi  3212  undif3ss  3225  symdifxor  3230  undif4  3306  iinuniss  3758  ordsucim  4244  suc11g  4300  qfto  4734  nntri3or  6095  reapcotr  7698  elnn0  8290  elnn1uz2  8694  nn01to3  8702  elxr  8850  lcmdvds  10461  mulgcddvds  10476  cncongr2  10486  bj-peano4  10750