Theorem orbi2d 795

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

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

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1d  796  orbi12d  798  dn1dc  966  xorbi2d  1422  eueq2dc  2976  r19.44mv  3586  rexprg  3718  rextpg  3720  exmidsssn  4285  exmidsssnc  4286  swopolem  4395  sowlin  4410  elsucg  4494  elsuc2g  4495  ordsoexmid  4653  poleloe  5127  funopsn  5816  isosolem  5947  freceq2  6537  brdifun  6705  pitric  7504  elinp  7657  prloc  7674  ltexprlemloc  7790  suplocexprlemloc  7904  ltsosr  7947  aptisr  7962  suplocsrlemb  7989  axpre-ltwlin  8066  axpre-suploclemres  8084  axpre-suploc  8085  gt0add  8716  apreap  8730  apreim  8746  elznn0  9457  elznn  9458  peano2z  9478  zindd  9561  elfzp1  10264  fzm1  10292  fzosplitsni  10436  cjap  11412  dvdslelemd  12349  zeo5  12394  lcmval  12580  lcmneg  12591  lcmass  12602  isprm6  12664  infpn2  13022  lringuplu  14154  domneq0  14230  znidom  14615  dedekindeulemloc  15287  dedekindeulemeu  15290  suplociccreex  15292  dedekindicclemloc  15296  dedekindicclemeu  15299  bj-charfunr  16131  bj-nn0sucALT  16299