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  3693  sbc2or  3774  r19.44zv  4479  elunsn  4659  rexprgf  4671  rextpg  4675  swopolem  5571  poleloe  6120  elsucg  6421  elsuc2g  6422  xpord2indlem  8144  brdifun  8747  brwdom  9579  isfin1a  10304  elgch  10634  suplem2pr  11065  axlttri  11304  mulcan1g  11888  elznn0  12601  elznn  12602  zindd  12692  rpneg  13039  dfle2  13161  fzm1  13622  fzosplitsni  13792  hashv01gt1  14361  zeo5  16373  bitsf1  16463  lcmval  16609  lcmneg  16620  lcmass  16631  isprm6  16731  infpn2  16931  irredmul  20387  lringuplu  20502  domneq0  20666  znfld  21519  quotval  26250  plydivlem4  26254  plydivex  26255  aalioulem2  26291  aalioulem5  26294  aalioulem6  26295  aaliou  26296  aaliou2  26298  aaliou2b  26299  elzs2  28302  elznns  28305  isinag  28763  axcontlem7  28895  hashecclwwlkn1  30004  eliccioo  32851  tlt2  32895  prmidl  33401  mxidlval  33422  rprmdvds  33480  sibfof  34318  ballotlemfc0  34471  ballotlemfcc  34472  satfvsucsuc  35333  satf0op  35345  fmlafvel  35353  isfmlasuc  35356  satfv1fvfmla1  35391  seglelin  36080  lineunray  36111  topdifinfeq  37314  wl-ifp4impr  37431  mblfinlem2  37628  pridl  38007  maxidlval  38009  ispridlc  38040  pridlc  38041  dmnnzd  38045  lcfl7N  41466  aomclem8  43032  fzuntgd  43429  orbi1r  44483  iccpartgtl  47388  iccpartleu  47390  clnbupgrel  47796  dfsclnbgr6  47819  lindslinindsimp2lem5  48386  lindslinindsimp2  48387  rrx2pnedifcoorneorr  48645