Theorem orbi2i 774

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

This proof depends on syntax axioms:   ↔ wb 105   ∨ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  orbi1i  775  orbi12i  776  orass  779  or4  783  or42  784  orordir  786  dcnnOLD  861  orbididc  966  3orcomb  1018  excxor  1427  xordc  1441  nf4dc  1722  nf4r  1723  19.44  1734  dveeq2  1868  dvelimALT  2070  dvelimfv  2071  dvelimor  2078  dcne  2431  unass  3386  undi  3479  undif3ss  3492  symdifxor  3497  undif4  3587  iinuniss  4095  ordsucim  4649  suc11g  4706  qfto  5180  nntri3or  6771  reapcotr  8934  elnn0  9576  elxnn0  9641  elnn1uz2  10022  nn01to3  10032  elxr  10194  xaddcom  10279  xnegdi  10286  xpncan  10289  xleadd1a  10291  hashf1lem2  11307  lcmdvds  12881  mulgcddvds  12896  cncongr2  12906  pythagtrip  13090  bj-peano4  17203  apdifflemr  17320