Theorem orbi2d 798

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

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

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1d  799  orbi12d  801  dn1dc  969  xorbi2d  1425  eueq2dc  2993  r19.44mv  3608  rexprg  3746  rextpg  3748  exmidsssn  4320  exmidsssnc  4321  swopolem  4431  sowlin  4446  elsucg  4530  elsuc2g  4531  ordsoexmid  4689  poleloe  5167  funopsn  5865  isosolem  6003  freceq2  6637  brdifun  6807  papcotr  7577  pitric  7652  elinp  7805  prloc  7822  ltexprlemloc  7938  suplocexprlemloc  8052  ltsosr  8095  aptisr  8110  suplocsrlemb  8137  axpre-ltwlin  8214  axpre-suploclemres  8232  axpre-suploc  8233  gt0add  8865  apreap  8879  apreim  8895  elznn0  9612  elznn  9613  peano2z  9633  zindd  9717  elfzp1  10431  fzm1  10459  fzosplitsni  10606  cjap  11619  dvdslelemd  12557  zeo5  12602  lcmval  12788  lcmneg  12799  lcmass  12810  isprm6  12872  ballotfilemfc0  13179  ballotfilemfcc  13180  infpn2  13294  gsumsplit0  14102  lringuplu  14444  domneq0  14522  znidom  14934  dedekindeulemloc  15613  dedekindeulemeu  15616  suplociccreex  15618  dedekindicclemloc  15622  dedekindicclemeu  15625  bj-charfunr  16719  bj-nn0sucALT  16887