Theorem orbi2d 791

Description: Deduction adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)

Hypothesis

Ref	Expression
orbid.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
orbi2d	⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒)))

Proof of Theorem orbi2d

Step	Hyp	Ref	Expression
1		orbid.1	. . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	biimpd 144	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	orim2d 789	. 2 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) → (𝜃 ∨ 𝜒)))
4	1	biimprd 158	. . 3 ⊢ (𝜑 → (𝜒 → 𝜓))
5	4	orim2d 789	. 2 ⊢ (𝜑 → ((𝜃 ∨ 𝜒) → (𝜃 ∨ 𝜓)))
6	3, 5	impbid 129	1 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒)))

Syntax hints:   → wi 4   ↔ wb 105   ∨ wo 709

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1d  792  orbi12d  794  dn1dc  962  xorbi2d  1391  eueq2dc  2937  r19.44mv  3545  rexprg  3674  rextpg  3676  exmidsssn  4235  exmidsssnc  4236  swopolem  4340  sowlin  4355  elsucg  4439  elsuc2g  4440  ordsoexmid  4598  poleloe  5069  isosolem  5871  freceq2  6451  brdifun  6619  pitric  7388  elinp  7541  prloc  7558  ltexprlemloc  7674  suplocexprlemloc  7788  ltsosr  7831  aptisr  7846  suplocsrlemb  7873  axpre-ltwlin  7950  axpre-suploclemres  7968  axpre-suploc  7969  gt0add  8600  apreap  8614  apreim  8630  elznn0  9341  elznn  9342  peano2z  9362  zindd  9444  elfzp1  10147  fzm1  10175  fzosplitsni  10311  cjap  11071  dvdslelemd  12008  zeo5  12053  lcmval  12231  lcmneg  12242  lcmass  12253  isprm6  12315  infpn2  12673  lringuplu  13752  domneq0  13828  znidom  14213  dedekindeulemloc  14855  dedekindeulemeu  14858  suplociccreex  14860  dedekindicclemloc  14864  dedekindicclemeu  14867  bj-charfunr  15456  bj-nn0sucALT  15624