Theorem orbi2d 780

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

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

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 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orbi1d  781  orbi12d  783  dn1dc  945  xorbi2d  1359  eueq2dc  2861  r19.44mv  3462  rexprg  3583  rextpg  3585  exmidsssn  4133  exmidsssnc  4134  swopolem  4235  sowlin  4250  elsucg  4334  elsuc2g  4335  ordsoexmid  4485  poleloe  4946  isosolem  5733  freceq2  6298  brdifun  6464  pitric  7153  elinp  7306  prloc  7323  ltexprlemloc  7439  suplocexprlemloc  7553  ltsosr  7596  aptisr  7611  suplocsrlemb  7638  axpre-ltwlin  7715  axpre-suploclemres  7733  axpre-suploc  7734  gt0add  8359  apreap  8373  apreim  8389  elznn0  9093  elznn  9094  peano2z  9114  zindd  9193  elfzp1  9883  fzm1  9911  fzosplitsni  10043  cjap  10710  dvdslelemd  11577  zeo5  11621  lcmval  11780  lcmneg  11791  lcmass  11802  isprm6  11861  dedekindeulemloc  12805  dedekindeulemeu  12808  suplociccreex  12810  dedekindicclemloc  12814  dedekindicclemeu  12817  bj-nn0sucALT  13347