Theorem orbi2d 914

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∨ wo 846

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 206  df-or 847

This theorem is referenced by:  orbi1d  915  orbi12d  917  eueq2  3705  sbc2or  3785  r19.44zv  4504  rexprgf  4698  rextpg  4704  swopolem  5600  poleloe  6137  elsucg  6437  elsuc2g  6438  xpord2indlem  8152  brdifun  8753  brwdom  9590  isfin1a  10315  elgch  10645  suplem2pr  11076  axlttri  11315  mulcan1g  11897  elznn0  12603  elznn  12604  zindd  12693  rpneg  13038  dfle2  13158  fzm1  13613  fzosplitsni  13775  hashv01gt1  14336  zeo5  16332  bitsf1  16420  lcmval  16562  lcmneg  16573  lcmass  16584  isprm6  16684  infpn2  16881  irredmul  20367  lringuplu  20480  domneq0  21243  znfld  21493  quotval  26226  plydivlem4  26230  plydivex  26231  aalioulem2  26267  aalioulem5  26270  aalioulem6  26271  aaliou  26272  aaliou2  26274  aaliou2b  26275  isinag  28641  axcontlem7  28780  hashecclwwlkn1  29886  elunsn  32307  eliccioo  32654  tlt2  32696  prmidl  33156  mxidlval  33174  sibfof  33960  ballotlemfc0  34112  ballotlemfcc  34113  satfvsucsuc  34975  satf0op  34987  fmlafvel  34995  isfmlasuc  34998  satfv1fvfmla1  35033  seglelin  35712  lineunray  35743  topdifinfeq  36829  wl-ifp4impr  36946  mblfinlem2  37131  pridl  37510  maxidlval  37512  ispridlc  37543  pridlc  37544  dmnnzd  37548  lcfl7N  40974  aomclem8  42485  fzuntgd  42888  orbi1r  43949  iccpartgtl  46766  iccpartleu  46768  lindslinindsimp2lem5  47530  lindslinindsimp2  47531  rrx2pnedifcoorneorr  47790