Theorem orbi2i 679

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

Syntax hints:   ↔ wb 98   ∨ wo 629

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 630

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  orbi1i  680  orbi12i  681  orass  684  or4  688  or42  689  orordir  691  testbitestn  823  orbididc  860  3orcomb  894  excxor  1269  xordc  1283  nf4dc  1560  nf4r  1561  19.44  1572  dveeq2  1696  dvelimALT  1886  dvelimfv  1887  dvelimor  1894  dcne  2216  unass  3100  undi  3185  undif3ss  3198  symdifxor  3203  undif4  3284  iinuniss  3737  ordsucim  4226  suc11g  4281  qfto  4714  nntri3or  6072  reapcotr  7589  elnn0  8183  elnn1uz2  8544  nn01to3  8552  elxr  8696  bj-peano4  10080