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  3664  sbc2or  3745  r19.44zv  4449  elunsn  4631  rexprgf  4643  rextpg  4647  swopolem  5529  poleloe  6073  elsucg  6371  elsuc2g  6372  xpord2indlem  8072  brdifun  8647  brwdom  9448  isfin1a  10178  elgch  10508  suplem2pr  10939  axlttri  11179  mulcan1g  11765  elznn0  12478  elznn  12479  zindd  12569  rpneg  12919  dfle2  13041  fzm1  13502  fzosplitsni  13674  hashv01gt1  14247  zeo5  16262  bitsf1  16352  lcmval  16498  lcmneg  16509  lcmass  16520  isprm6  16620  infpn2  16820  irredmul  20342  lringuplu  20454  domneq0  20618  znfld  21492  quotval  26222  plydivlem4  26226  plydivex  26227  aalioulem2  26263  aalioulem5  26266  aalioulem6  26267  aaliou  26268  aaliou2  26270  aaliou2b  26271  elzs2  28318  elznns  28321  isinag  28811  axcontlem7  28943  hashecclwwlkn1  30049  eliccioo  32903  tlt2  32942  prmidl  33397  mxidlval  33418  rprmdvds  33476  sibfof  34345  ballotlemfc0  34498  ballotlemfcc  34499  satfvsucsuc  35401  satf0op  35413  fmlafvel  35421  isfmlasuc  35424  satfv1fvfmla1  35459  seglelin  36150  lineunray  36181  topdifinfeq  37384  wl-ifp4impr  37501  mblfinlem2  37698  pridl  38077  maxidlval  38079  ispridlc  38110  pridlc  38111  dmnnzd  38115  lcfl7N  41540  aomclem8  43094  fzuntgd  43491  orbi1r  44543  iccpartgtl  47457  iccpartleu  47459  clnbupgrel  47865  dfsclnbgr6  47889  lindslinindsimp2lem5  48494  lindslinindsimp2  48495  rrx2pnedifcoorneorr  48749