Theorem orbi2d 791

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

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

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1d  792  orbi12d  794  dn1dc  962  xorbi2d  1399  eueq2dc  2945  r19.44mv  3554  rexprg  3684  rextpg  3686  exmidsssn  4245  exmidsssnc  4246  swopolem  4350  sowlin  4365  elsucg  4449  elsuc2g  4450  ordsoexmid  4608  poleloe  5079  isosolem  5883  freceq2  6469  brdifun  6637  pitric  7416  elinp  7569  prloc  7586  ltexprlemloc  7702  suplocexprlemloc  7816  ltsosr  7859  aptisr  7874  suplocsrlemb  7901  axpre-ltwlin  7978  axpre-suploclemres  7996  axpre-suploc  7997  gt0add  8628  apreap  8642  apreim  8658  elznn0  9369  elznn  9370  peano2z  9390  zindd  9473  elfzp1  10176  fzm1  10204  fzosplitsni  10345  cjap  11136  dvdslelemd  12073  zeo5  12118  lcmval  12304  lcmneg  12315  lcmass  12326  isprm6  12388  infpn2  12746  lringuplu  13876  domneq0  13952  znidom  14337  dedekindeulemloc  15009  dedekindeulemeu  15012  suplociccreex  15014  dedekindicclemloc  15018  dedekindicclemeu  15021  bj-charfunr  15610  bj-nn0sucALT  15778