Theorem orbi2d 916

Description: Deduction adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 21-Jun-1993.)

Hypothesis

Ref	Expression
bid.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
orbi2d	⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒)))

Proof of Theorem orbi2d

Step	Hyp	Ref	Expression
1		bid.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	imbi2d 340	. 2 ⊢ (𝜑 → ((¬ 𝜃 → 𝜓) ↔ (¬ 𝜃 → 𝜒)))
3		df-or 849	. 2 ⊢ ((𝜃 ∨ 𝜓) ↔ (¬ 𝜃 → 𝜓))
4		df-or 849	. 2 ⊢ ((𝜃 ∨ 𝜒) ↔ (¬ 𝜃 → 𝜒))
5	2, 3, 4	3bitr4g 314	1 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∨ wo 848

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-or 849

This theorem is referenced by:  orbi1d  917  orbi12d  919  eueq2  3656  sbc2or  3737  r19.44zv  4449  elunsn  4627  rexprgf  4639  rextpg  4643  swopolem  5549  poleloe  6094  elsucg  6393  elsuc2g  6394  xpord2indlem  8097  brdifun  8674  brwdom  9482  isfin1a  10214  elgch  10545  suplem2pr  10976  axlttri  11217  mulcan1g  11803  elznn0  12539  elznn  12540  zindd  12630  rpneg  12976  dfle2  13098  fzm1  13561  fzosplitsni  13734  hashv01gt1  14307  zeo5  16325  bitsf1  16415  lcmval  16561  lcmneg  16572  lcmass  16583  isprm6  16684  infpn2  16884  irredmul  20409  lringuplu  20521  domneq0  20685  znfld  21540  quotval  26258  plydivlem4  26262  plydivex  26263  aalioulem2  26299  aalioulem5  26302  aalioulem6  26303  aaliou  26304  aaliou2  26306  aaliou2b  26307  elzs2  28391  elznns  28394  isinag  28906  axcontlem7  29039  hashecclwwlkn1  30147  eliccioo  32990  tlt2  33029  prmidl  33500  mxidlval  33521  rprmdvds  33579  sibfof  34484  ballotlemfc0  34637  ballotlemfcc  34638  satfvsucsuc  35547  satf0op  35559  fmlafvel  35567  isfmlasuc  35570  satfv1fvfmla1  35605  seglelin  36298  lineunray  36329  topdifinfeq  37666  wl-ifp4impr  37783  mblfinlem2  37979  pridl  38358  maxidlval  38360  ispridlc  38391  pridlc  38392  dmnnzd  38396  lcfl7N  41947  aomclem8  43489  fzuntgd  43885  orbi1r  44937  iccpartgtl  47886  iccpartleu  47888  nprmmul3  47989  clnbupgrel  48310  dfsclnbgr6  48334  lindslinindsimp2lem5  48938  lindslinindsimp2  48939  rrx2pnedifcoorneorr  49193