Theorem orbi2d 790

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

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

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 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1d  791  orbi12d  793  dn1dc  960  xorbi2d  1380  eueq2dc  2911  r19.44mv  3518  rexprg  3645  rextpg  3647  exmidsssn  4203  exmidsssnc  4204  swopolem  4306  sowlin  4321  elsucg  4405  elsuc2g  4406  ordsoexmid  4562  poleloe  5029  isosolem  5825  freceq2  6394  brdifun  6562  pitric  7320  elinp  7473  prloc  7490  ltexprlemloc  7606  suplocexprlemloc  7720  ltsosr  7763  aptisr  7778  suplocsrlemb  7805  axpre-ltwlin  7882  axpre-suploclemres  7900  axpre-suploc  7901  gt0add  8530  apreap  8544  apreim  8560  elznn0  9268  elznn  9269  peano2z  9289  zindd  9371  elfzp1  10072  fzm1  10100  fzosplitsni  10235  cjap  10915  dvdslelemd  11849  zeo5  11893  lcmval  12063  lcmneg  12074  lcmass  12085  isprm6  12147  infpn2  12457  lringuplu  13337  dedekindeulemloc  14100  dedekindeulemeu  14103  suplociccreex  14105  dedekindicclemloc  14109  dedekindicclemeu  14112  bj-charfunr  14565  bj-nn0sucALT  14733