Theorem orbi2d 797

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

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

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 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1d  798  orbi12d  800  dn1dc  968  xorbi2d  1424  eueq2dc  2979  r19.44mv  3589  rexprg  3721  rextpg  3723  exmidsssn  4292  exmidsssnc  4293  swopolem  4402  sowlin  4417  elsucg  4501  elsuc2g  4502  ordsoexmid  4660  poleloe  5136  funopsn  5829  isosolem  5964  freceq2  6558  brdifun  6728  pitric  7540  elinp  7693  prloc  7710  ltexprlemloc  7826  suplocexprlemloc  7940  ltsosr  7983  aptisr  7998  suplocsrlemb  8025  axpre-ltwlin  8102  axpre-suploclemres  8120  axpre-suploc  8121  gt0add  8752  apreap  8766  apreim  8782  elznn0  9493  elznn  9494  peano2z  9514  zindd  9597  elfzp1  10306  fzm1  10334  fzosplitsni  10480  cjap  11466  dvdslelemd  12403  zeo5  12448  lcmval  12634  lcmneg  12645  lcmass  12656  isprm6  12718  infpn2  13076  lringuplu  14209  domneq0  14285  znidom  14670  dedekindeulemloc  15342  dedekindeulemeu  15345  suplociccreex  15347  dedekindicclemloc  15351  dedekindicclemeu  15354  bj-charfunr  16405  bj-nn0sucALT  16573