Theorem orbi2d 780

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 143	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	orim2d 778	. 2 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) → (𝜃 ∨ 𝜒)))
4	1	biimprd 157	. . 3 ⊢ (𝜑 → (𝜒 → 𝜓))
5	4	orim2d 778	. 2 ⊢ (𝜑 → ((𝜃 ∨ 𝜒) → (𝜃 ∨ 𝜓)))
6	3, 5	impbid 128	1 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒)))

Syntax hints:   → wi 4   ↔ wb 104   ∨ wo 698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orbi1d  781  orbi12d  783  dn1dc  950  xorbi2d  1370  eueq2dc  2899  r19.44mv  3503  rexprg  3628  rextpg  3630  exmidsssn  4181  exmidsssnc  4182  swopolem  4283  sowlin  4298  elsucg  4382  elsuc2g  4383  ordsoexmid  4539  poleloe  5003  isosolem  5792  freceq2  6361  brdifun  6528  pitric  7262  elinp  7415  prloc  7432  ltexprlemloc  7548  suplocexprlemloc  7662  ltsosr  7705  aptisr  7720  suplocsrlemb  7747  axpre-ltwlin  7824  axpre-suploclemres  7842  axpre-suploc  7843  gt0add  8471  apreap  8485  apreim  8501  elznn0  9206  elznn  9207  peano2z  9227  zindd  9309  elfzp1  10007  fzm1  10035  fzosplitsni  10170  cjap  10848  dvdslelemd  11781  zeo5  11825  lcmval  11995  lcmneg  12006  lcmass  12017  isprm6  12079  infpn2  12389  dedekindeulemloc  13237  dedekindeulemeu  13240  suplociccreex  13242  dedekindicclemloc  13246  dedekindicclemeu  13249  bj-charfunr  13692  bj-nn0sucALT  13860