Theorem orbi2i 767

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

Syntax hints:   ↔ wb 105   ∨ wo 713

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1i  768  orbi12i  769  orass  772  or4  776  or42  777  orordir  779  dcnnOLD  854  orbididc  959  3orcomb  1011  excxor  1420  xordc  1434  nf4dc  1716  nf4r  1717  19.44  1728  dveeq2  1861  dvelimALT  2061  dvelimfv  2062  dvelimor  2069  dcne  2411  unass  3361  undi  3452  undif3ss  3465  symdifxor  3470  undif4  3554  iinuniss  4047  ordsucim  4591  suc11g  4648  qfto  5117  nntri3or  6637  reapcotr  8741  elnn0  9367  elxnn0  9430  elnn1uz2  9798  nn01to3  9808  elxr  9968  xaddcom  10053  xnegdi  10060  xpncan  10063  xleadd1a  10065  lcmdvds  12596  mulgcddvds  12611  cncongr2  12621  pythagtrip  12801  bj-peano4  16276  apdifflemr  16374