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  8903  apreap  8917  apreim  8933  elznn0  9663  elznn  9664  peano2z  9684  zindd  9768  elfzp1  10489  fzm1  10517  fzosplitsni  10664  cjap  11686  dvdslelemd  12626  zeo5  12671  lcmval  12857  lcmneg  12868  lcmass  12879  isprm6  12942  ballotfilemfc0  13281  ballotfilemfcc  13282  infpn2  13396  gzsumsplit0  14197  lringuplu  14552  domneq0  14630  znidom  15041  dedekindeulemloc  15769  dedekindeulemeu  15772  suplociccreex  15774  dedekindicclemloc  15778  dedekindicclemeu  15781  bj-charfunr  16934  bj-nn0sucALT  17102