Theorem orbi2d 802

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   ∨ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  orbi1d  803  orbi12d  805  dn1dc  973  xorbi2d  1429  eueq2dc  2999  r19.44mv  3622  rexprg  3761  rextpg  3763  exmidsssn  4339  exmidsssnc  4340  swopolem  4450  sowlin  4465  elsucg  4549  elsuc2g  4550  ordsoexmid  4709  poleloe  5187  funopsn  5891  isosolem  6030  freceq2  6664  brdifun  6834  papcotr  7613  pitric  7688  elinp  7841  prloc  7858  ltexprlemloc  7974  suplocexprlemloc  8088  ltsosr  8131  aptisr  8146  suplocsrlemb  8173  axpre-ltwlin  8250  axpre-suploclemres  8268  axpre-suploc  8269  gt0add  8901  apreap  8915  apreim  8931  elznn0  9659  elznn  9660  peano2z  9680  zindd  9764  elfzp1  10479  fzm1  10507  fzosplitsni  10654  cjap  11672  dvdslelemd  12610  zeo5  12655  lcmval  12841  lcmneg  12852  lcmass  12863  isprm6  12925  ballotfilemfc0  13232  ballotfilemfcc  13233  infpn2  13347  gzsumsplit0  14148  lringuplu  14503  domneq0  14581  znidom  14992  dedekindeulemloc  15720  dedekindeulemeu  15723  suplociccreex  15725  dedekindicclemloc  15729  dedekindicclemeu  15732  bj-charfunr  16836  bj-nn0sucALT  17004