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  1391  eueq2dc  2925  r19.44mv  3532  rexprg  3659  rextpg  3661  exmidsssn  4220  exmidsssnc  4221  swopolem  4323  sowlin  4338  elsucg  4422  elsuc2g  4423  ordsoexmid  4579  poleloe  5046  isosolem  5845  freceq2  6417  brdifun  6585  pitric  7349  elinp  7502  prloc  7519  ltexprlemloc  7635  suplocexprlemloc  7749  ltsosr  7792  aptisr  7807  suplocsrlemb  7834  axpre-ltwlin  7911  axpre-suploclemres  7929  axpre-suploc  7930  gt0add  8559  apreap  8573  apreim  8589  elznn0  9297  elznn  9298  peano2z  9318  zindd  9400  elfzp1  10101  fzm1  10129  fzosplitsni  10264  cjap  10946  dvdslelemd  11880  zeo5  11924  lcmval  12094  lcmneg  12105  lcmass  12116  isprm6  12178  infpn2  12506  lringuplu  13540  dedekindeulemloc  14549  dedekindeulemeu  14552  suplociccreex  14554  dedekindicclemloc  14558  dedekindicclemeu  14561  bj-charfunr  15015  bj-nn0sucALT  15183