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  4286  exmidsssnc  4287  swopolem  4396  sowlin  4411  elsucg  4495  elsuc2g  4496  ordsoexmid  4654  poleloe  5128  funopsn  5819  isosolem  5954  freceq2  6545  brdifun  6715  pitric  7519  elinp  7672  prloc  7689  ltexprlemloc  7805  suplocexprlemloc  7919  ltsosr  7962  aptisr  7977  suplocsrlemb  8004  axpre-ltwlin  8081  axpre-suploclemres  8099  axpre-suploc  8100  gt0add  8731  apreap  8745  apreim  8761  elznn0  9472  elznn  9473  peano2z  9493  zindd  9576  elfzp1  10280  fzm1  10308  fzosplitsni  10453  cjap  11432  dvdslelemd  12369  zeo5  12414  lcmval  12600  lcmneg  12611  lcmass  12622  isprm6  12684  infpn2  13042  lringuplu  14175  domneq0  14251  znidom  14636  dedekindeulemloc  15308  dedekindeulemeu  15311  suplociccreex  15313  dedekindicclemloc  15317  dedekindicclemeu  15320  bj-charfunr  16228  bj-nn0sucALT  16396