Theorem orbi2d 929

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 343	. 2 ⊢ (𝜑 → ((¬ 𝜃 → 𝜓) ↔ (¬ 𝜃 → 𝜒)))
3		df-or 862	. 2 ⊢ ((𝜃 ∨ 𝜓) ↔ (¬ 𝜃 → 𝜓))
4		df-or 862	. 2 ⊢ ((𝜃 ∨ 𝜒) ↔ (¬ 𝜃 → 𝜒))
5	2, 3, 4	3bitr4g 317	1 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  orbi1d  930  orbi12d  932  eueq2  3671  sbc2or  3751  r19.44zv  4468  elunsn  4645  rexprgf  4657  rextpg  4661  swopolem  5576  poleloe  6143  elsucg  6459  elsuc2g  6460  xpord2indlem  8201  brdifun  8786  brwdom  9598  isfin1a  10409  elgch  10746  suplem2pr  11177  axlttri  11420  mulcan1g  12009  elznn0  12748  elznn  12749  zindd  12840  rpneg  13194  dfle2  13316  fzm1  13781  fzosplitsni  13954  hashv01gt1  14530  zeo5  16570  bitsf1  16660  lcmval  16811  lcmneg  16822  lcmass  16833  isprm6  16934  infpn2  17135  irredmul  20710  lringuplu  20847  domneq0  21011  prmidl  21672  prmidlprop  21683  znfld  21921  quotval  26668  plydivlem4  26672  plydivex  26673  aalioulem2  26717  aalioulem5  26720  aalioulem6  26721  aaliou  26722  aaliou2  26724  aaliou2b  26725  elzs2  28842  elznns  28845  elplng  29315  plngcplem  29320  isinag  29414  brprlng  29473  axcontlem7  29605  hashecclwwlkn1  30725  eliccioo  33593  tlt2  33626  isedom  33953  edomediv  33955  mxidlval  34090  rprmdvds  34155  sibfof  35083  ballotlemfc0  35236  ballotlemfcc  35237  onf1oracwevd  36093  satfvsucsuc  36338  satf0op  36350  fmlafvel  36358  isfmlasuc  36361  satfv1fvfmla1  36396  seglelin  37096  lineunray  37127  topdifinfeq  38541  wl-ifp4impr  38658  mblfinlem2  38844  varprop  38910  negprop  38911  impprop  38912  dfprop2  38914  pridl  39237  maxidlval  39239  ispridlc  39270  pridlc  39271  dmnnzd  39275  lcfl7N  42824  aomclem8  44329  fzuntgd  44720  orbi1r  45753  iccpartgtl  48781  iccpartleu  48783  nprmmul3  48884  clnbupgrel  49205  dfsclnbgr6  49229  idomnzd  49774  lindslinindsimp2lem5  49905  lindslinindsimp2  49906  rrx2pnedifcoorneorr  50161