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  3670  sbc2or  3751  r19.44zv  4464  elunsn  4642  rexprgf  4654  rextpg  4658  swopolem  5550  poleloe  6096  elsucg  6395  elsuc2g  6396  xpord2indlem  8099  brdifun  8676  brwdom  9484  isfin1a  10214  elgch  10545  suplem2pr  10976  axlttri  11216  mulcan1g  11802  elznn0  12515  elznn  12516  zindd  12605  rpneg  12951  dfle2  13073  fzm1  13535  fzosplitsni  13707  hashv01gt1  14280  zeo5  16295  bitsf1  16385  lcmval  16531  lcmneg  16542  lcmass  16553  isprm6  16653  infpn2  16853  irredmul  20377  lringuplu  20489  domneq0  20653  znfld  21527  quotval  26268  plydivlem4  26272  plydivex  26273  aalioulem2  26309  aalioulem5  26312  aalioulem6  26313  aaliou  26314  aaliou2  26316  aaliou2b  26317  elzs2  28407  elznns  28410  isinag  28922  axcontlem7  29055  hashecclwwlkn1  30164  eliccioo  33023  tlt2  33062  prmidl  33533  mxidlval  33554  rprmdvds  33612  sibfof  34518  ballotlemfc0  34671  ballotlemfcc  34672  satfvsucsuc  35581  satf0op  35593  fmlafvel  35601  isfmlasuc  35604  satfv1fvfmla1  35639  seglelin  36332  lineunray  36363  topdifinfeq  37605  wl-ifp4impr  37722  mblfinlem2  37909  pridl  38288  maxidlval  38290  ispridlc  38321  pridlc  38322  dmnnzd  38326  lcfl7N  41877  aomclem8  43418  fzuntgd  43814  orbi1r  44866  iccpartgtl  47786  iccpartleu  47788  clnbupgrel  48194  dfsclnbgr6  48218  lindslinindsimp2lem5  48822  lindslinindsimp2  48823  rrx2pnedifcoorneorr  49077