Theorem orbi2d 779

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

Syntax hints:   → wi 4   ↔ wb 104   ∨ wo 697

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orbi1d  780  orbi12d  782  dn1dc  944  xorbi2d  1358  eueq2dc  2857  r19.44mv  3457  rexprg  3575  rextpg  3577  exmidsssn  4125  exmidsssnc  4126  swopolem  4227  sowlin  4242  elsucg  4326  elsuc2g  4327  ordsoexmid  4477  poleloe  4938  isosolem  5725  freceq2  6290  brdifun  6456  pitric  7129  elinp  7282  prloc  7299  ltexprlemloc  7415  suplocexprlemloc  7529  ltsosr  7572  aptisr  7587  suplocsrlemb  7614  axpre-ltwlin  7691  axpre-suploclemres  7709  axpre-suploc  7710  gt0add  8335  apreap  8349  apreim  8365  elznn0  9069  elznn  9070  peano2z  9090  zindd  9169  elfzp1  9852  fzm1  9880  fzosplitsni  10012  cjap  10678  dvdslelemd  11541  zeo5  11585  lcmval  11744  lcmneg  11755  lcmass  11766  isprm6  11825  dedekindeulemloc  12766  dedekindeulemeu  12769  suplociccreex  12771  dedekindicclemloc  12775  dedekindicclemeu  12778  bj-nn0sucALT  13176