Theorem orbi2i 666

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

Syntax hints:   ↔ wb 98   ∨ wo 616

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 617

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  orbi1i  667  orbi12i  668  orass  671  or4  675  or42  676  orordir  678  testbitestn  732  orbididc  848  3orcomb  882  excxor  1254  xordc  1266  nf4dc  1542  nf4r  1543  19.44  1554  dveeq2  1678  dvelimALT  1868  dvelimfv  1869  dvelimor  1876  exmidnedc  2195  unass  3077  undi  3162  undif3ss  3175  symdifxor  3180  undif4  3261  iinuniss  3711  ordsucim  4176  suc11g  4219  qfto  4641  nntri3or  5987  bj-peano4  7324