Theorem orbi2d 915

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

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

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 848

This theorem is referenced by:  orbi1d  916  orbi12d  918  eueq2  3718  sbc2or  3799  r19.44zv  4509  elunsn  4687  rexprgf  4699  rextpg  4703  swopolem  5606  poleloe  6153  elsucg  6453  elsuc2g  6454  xpord2indlem  8170  brdifun  8773  brwdom  9604  isfin1a  10329  elgch  10659  suplem2pr  11090  axlttri  11329  mulcan1g  11913  elznn0  12625  elznn  12626  zindd  12716  rpneg  13064  dfle2  13185  fzm1  13643  fzosplitsni  13813  hashv01gt1  14380  zeo5  16389  bitsf1  16479  lcmval  16625  lcmneg  16636  lcmass  16647  isprm6  16747  infpn2  16946  irredmul  20445  lringuplu  20560  domneq0  20724  znfld  21596  quotval  26348  plydivlem4  26352  plydivex  26353  aalioulem2  26389  aalioulem5  26392  aalioulem6  26393  aaliou  26394  aaliou2  26396  aaliou2b  26397  elzs2  28399  elznns  28402  isinag  28860  axcontlem7  28999  hashecclwwlkn1  30105  eliccioo  32897  tlt2  32943  prmidl  33447  mxidlval  33468  rprmdvds  33526  sibfof  34321  ballotlemfc0  34473  ballotlemfcc  34474  satfvsucsuc  35349  satf0op  35361  fmlafvel  35369  isfmlasuc  35372  satfv1fvfmla1  35407  seglelin  36097  lineunray  36128  topdifinfeq  37332  wl-ifp4impr  37449  mblfinlem2  37644  pridl  38023  maxidlval  38025  ispridlc  38056  pridlc  38057  dmnnzd  38061  lcfl7N  41483  aomclem8  43049  fzuntgd  43447  orbi1r  44507  iccpartgtl  47350  iccpartleu  47352  clnbupgrel  47758  dfsclnbgr6  47781  lindslinindsimp2lem5  48307  lindslinindsimp2  48308  rrx2pnedifcoorneorr  48566