Theorem orbi2d 798

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

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

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1d  799  orbi12d  801  dn1dc  969  xorbi2d  1425  eueq2dc  2980  r19.44mv  3591  rexprg  3725  rextpg  3727  exmidsssn  4298  exmidsssnc  4299  swopolem  4408  sowlin  4423  elsucg  4507  elsuc2g  4508  ordsoexmid  4666  poleloe  5143  funopsn  5838  isosolem  5975  freceq2  6602  brdifun  6772  pitric  7584  elinp  7737  prloc  7754  ltexprlemloc  7870  suplocexprlemloc  7984  ltsosr  8027  aptisr  8042  suplocsrlemb  8069  axpre-ltwlin  8146  axpre-suploclemres  8164  axpre-suploc  8165  gt0add  8795  apreap  8809  apreim  8825  elznn0  9538  elznn  9539  peano2z  9559  zindd  9642  elfzp1  10352  fzm1  10380  fzosplitsni  10527  cjap  11529  dvdslelemd  12467  zeo5  12512  lcmval  12698  lcmneg  12709  lcmass  12720  isprm6  12782  infpn2  13140  gsumsplit0  13996  lringuplu  14274  domneq0  14351  znidom  14736  dedekindeulemloc  15413  dedekindeulemeu  15416  suplociccreex  15418  dedekindicclemloc  15422  dedekindicclemeu  15425  bj-charfunr  16509  bj-nn0sucALT  16677