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  2977  r19.44mv  3587  rexprg  3719  rextpg  3721  exmidsssn  4290  exmidsssnc  4291  swopolem  4400  sowlin  4415  elsucg  4499  elsuc2g  4500  ordsoexmid  4658  poleloe  5134  funopsn  5825  isosolem  5960  freceq2  6554  brdifun  6724  pitric  7531  elinp  7684  prloc  7701  ltexprlemloc  7817  suplocexprlemloc  7931  ltsosr  7974  aptisr  7989  suplocsrlemb  8016  axpre-ltwlin  8093  axpre-suploclemres  8111  axpre-suploc  8112  gt0add  8743  apreap  8757  apreim  8773  elznn0  9484  elznn  9485  peano2z  9505  zindd  9588  elfzp1  10297  fzm1  10325  fzosplitsni  10471  cjap  11457  dvdslelemd  12394  zeo5  12439  lcmval  12625  lcmneg  12636  lcmass  12647  isprm6  12709  infpn2  13067  lringuplu  14200  domneq0  14276  znidom  14661  dedekindeulemloc  15333  dedekindeulemeu  15336  suplociccreex  15338  dedekindicclemloc  15342  dedekindicclemeu  15345  bj-charfunr  16341  bj-nn0sucALT  16509