Theorem orbi2i 678

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 113	. . 3 ⊢ (φ → ψ)
3	2	orim2i 677	. 2 ⊢ ((χ ∨ φ) → (χ ∨ ψ))
4	1	biimpri 124	. . 3 ⊢ (ψ → φ)
5	4	orim2i 677	. 2 ⊢ ((χ ∨ ψ) → (χ ∨ φ))
6	3, 5	impbii 117	1 ⊢ ((χ ∨ φ) ↔ (χ ∨ ψ))

Syntax hints:   ↔ wb 98   ∨ wo 628

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  orbi1i  679  orbi12i  680  orass  683  or4  687  or42  688  orordir  690  testbitestn  822  orbididc  859  3orcomb  893  excxor  1268  xordc  1280  nf4dc  1557  nf4r  1558  19.44  1569  dveeq2  1693  dvelimALT  1883  dvelimfv  1884  dvelimor  1891  dcne  2211  unass  3094  undi  3179  undif3ss  3192  symdifxor  3197  undif4  3278  iinuniss  3728  ordsucim  4192  suc11g  4235  qfto  4657  nntri3or  6011  reapcotr  7362  elnn0  7939  elnn1uz2  8300  nn01to3  8308  elxr  8446  bj-peano4  9389