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  3546  rexprg  3675  rextpg  3677  exmidsssn  4236  exmidsssnc  4237  swopolem  4341  sowlin  4356  elsucg  4440  elsuc2g  4441  ordsoexmid  4599  poleloe  5070  isosolem  5874  freceq2  6460  brdifun  6628  pitric  7407  elinp  7560  prloc  7577  ltexprlemloc  7693  suplocexprlemloc  7807  ltsosr  7850  aptisr  7865  suplocsrlemb  7892  axpre-ltwlin  7969  axpre-suploclemres  7987  axpre-suploc  7988  gt0add  8619  apreap  8633  apreim  8649  elznn0  9360  elznn  9361  peano2z  9381  zindd  9463  elfzp1  10166  fzm1  10194  fzosplitsni  10330  cjap  11090  dvdslelemd  12027  zeo5  12072  lcmval  12258  lcmneg  12269  lcmass  12280  isprm6  12342  infpn2  12700  lringuplu  13830  domneq0  13906  znidom  14291  dedekindeulemloc  14963  dedekindeulemeu  14966  suplociccreex  14968  dedekindicclemloc  14972  dedekindicclemeu  14975  bj-charfunr  15564  bj-nn0sucALT  15732