Theorem orbi2i 764

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

Syntax hints:   ↔ wb 105   ∨ wo 710

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 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1i  765  orbi12i  766  orass  769  or4  773  or42  774  orordir  776  dcnnOLD  851  orbididc  956  3orcomb  990  excxor  1398  xordc  1412  nf4dc  1694  nf4r  1695  19.44  1706  dveeq2  1839  dvelimALT  2039  dvelimfv  2040  dvelimor  2047  dcne  2388  unass  3334  undi  3425  undif3ss  3438  symdifxor  3443  undif4  3527  iinuniss  4016  ordsucim  4556  suc11g  4613  qfto  5081  nntri3or  6592  reapcotr  8691  elnn0  9317  elxnn0  9380  elnn1uz2  9748  nn01to3  9758  elxr  9918  xaddcom  10003  xnegdi  10010  xpncan  10013  xleadd1a  10015  lcmdvds  12476  mulgcddvds  12491  cncongr2  12501  pythagtrip  12681  bj-peano4  16029  apdifflemr  16127