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  7614  pitric  7689  elinp  7842  prloc  7859  ltexprlemloc  7975  suplocexprlemloc  8089  ltsosr  8132  aptisr  8147  suplocsrlemb  8174  axpre-ltwlin  8251  axpre-suploclemres  8269  axpre-suploc  8270  gt0add  8904  apreap  8918  apreim  8934  elznn0  9664  elznn  9665  peano2z  9685  zindd  9769  elfzp1  10490  fzm1  10518  fzosplitsni  10665  cjap  11688  dvdslelemd  12629  zeo5  12674  lcmval  12860  lcmneg  12871  lcmass  12882  isprm6  12945  ballotfilemfc0  13284  ballotfilemfcc  13285  infpn2  13399  gzsumsplit0  14232  lringuplu  14587  domneq0  14665  znidom  15076  dedekindeulemloc  15811  dedekindeulemeu  15814  suplociccreex  15816  dedekindicclemloc  15820  dedekindicclemeu  15823  bj-charfunr  17002  bj-nn0sucALT  17170