Theorem orbi2d 926

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∨ wo 858

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 209  df-or 859

This theorem is referenced by:  orbi1d  927  orbi12d  929  eueq2  3671  sbc2or  3751  r19.44zv  4460  elunsn  4639  rexprgf  4651  rextpg  4655  swopolem  5561  poleloe  6114  elsucg  6411  elsuc2g  6412  xpord2indlem  8121  brdifun  8703  brwdom  9509  isfin1a  10243  elgch  10574  suplem2pr  11005  axlttri  11248  mulcan1g  11834  elznn0  12577  elznn  12578  zindd  12668  rpneg  13021  dfle2  13143  fzm1  13606  fzosplitsni  13779  hashv01gt1  14352  zeo5  16381  bitsf1  16471  lcmval  16617  lcmneg  16628  lcmass  16639  isprm6  16740  infpn2  16940  irredmul  20465  lringuplu  20581  domneq0  20745  znfld  21600  quotval  26344  plydivlem4  26348  plydivex  26349  aalioulem2  26385  aalioulem5  26388  aalioulem6  26389  aaliou  26390  aaliou2  26392  aaliou2b  26393  elzs2  28480  elznns  28483  isinag  28995  axcontlem7  29128  hashecclwwlkn1  30236  eliccioo  33069  tlt2  33108  prmidl  33587  prmidlprop  33596  mxidlval  33610  rprmdvds  33676  sibfof  34598  ballotlemfc0  34751  ballotlemfcc  34752  satfvsucsuc  35676  satf0op  35688  fmlafvel  35696  isfmlasuc  35699  satfv1fvfmla1  35734  seglelin  36427  lineunray  36458  topdifinfeq  37805  wl-ifp4impr  37922  mblfinlem2  38118  pridl  38497  maxidlval  38499  ispridlc  38530  pridlc  38531  dmnnzd  38535  lcfl7N  42086  aomclem8  43599  fzuntgd  43995  orbi1r  45047  iccpartgtl  47993  iccpartleu  47995  nprmmul3  48096  clnbupgrel  48417  dfsclnbgr6  48441  lindslinindsimp2lem5  49045  lindslinindsimp2  49046  rrx2pnedifcoorneorr  49300