Theorem orbi2i 769

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

Syntax hints:   ↔ wb 105   ∨ wo 715

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 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1i  770  orbi12i  771  orass  774  or4  778  or42  779  orordir  781  dcnnOLD  856  orbididc  961  3orcomb  1013  excxor  1422  xordc  1436  nf4dc  1718  nf4r  1719  19.44  1730  dveeq2  1863  dvelimALT  2063  dvelimfv  2064  dvelimor  2071  dcne  2413  unass  3364  undi  3455  undif3ss  3468  symdifxor  3473  undif4  3557  iinuniss  4053  ordsucim  4598  suc11g  4655  qfto  5126  nntri3or  6661  reapcotr  8778  elnn0  9404  elxnn0  9467  elnn1uz2  9841  nn01to3  9851  elxr  10011  xaddcom  10096  xnegdi  10103  xpncan  10106  xleadd1a  10108  lcmdvds  12669  mulgcddvds  12684  cncongr2  12694  pythagtrip  12874  bj-peano4  16601  apdifflemr  16702