Theorem orbi2d 792

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

Syntax hints:   → wi 4   ↔ wb 105   ∨ wo 710

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 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1d  793  orbi12d  795  dn1dc  963  xorbi2d  1400  eueq2dc  2950  r19.44mv  3559  rexprg  3690  rextpg  3692  exmidsssn  4254  exmidsssnc  4255  swopolem  4360  sowlin  4375  elsucg  4459  elsuc2g  4460  ordsoexmid  4618  poleloe  5091  funopsn  5775  isosolem  5906  freceq2  6492  brdifun  6660  pitric  7454  elinp  7607  prloc  7624  ltexprlemloc  7740  suplocexprlemloc  7854  ltsosr  7897  aptisr  7912  suplocsrlemb  7939  axpre-ltwlin  8016  axpre-suploclemres  8034  axpre-suploc  8035  gt0add  8666  apreap  8680  apreim  8696  elznn0  9407  elznn  9408  peano2z  9428  zindd  9511  elfzp1  10214  fzm1  10242  fzosplitsni  10386  cjap  11292  dvdslelemd  12229  zeo5  12274  lcmval  12460  lcmneg  12471  lcmass  12482  isprm6  12544  infpn2  12902  lringuplu  14033  domneq0  14109  znidom  14494  dedekindeulemloc  15166  dedekindeulemeu  15169  suplociccreex  15171  dedekindicclemloc  15175  dedekindicclemeu  15178  bj-charfunr  15884  bj-nn0sucALT  16052