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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∨ wo 846

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 206  df-or 847

This theorem is referenced by:  orbi1d  916  orbi12d  918  eueq2  3707  sbc2or  3787  r19.44zv  4504  rexprgf  4698  rextpg  4704  swopolem  5599  poleloe  6133  elsucg  6433  elsuc2g  6434  xpord2indlem  8133  brdifun  8732  brwdom  9562  isfin1a  10287  elgch  10617  suplem2pr  11048  axlttri  11285  mulcan1g  11867  elznn0  12573  elznn  12574  zindd  12663  rpneg  13006  dfle2  13126  fzm1  13581  fzosplitsni  13743  hashv01gt1  14305  zeo5  16299  bitsf1  16387  lcmval  16529  lcmneg  16540  lcmass  16551  isprm6  16651  infpn2  16846  irredmul  20243  lringuplu  20314  domneq0  20913  znfld  21116  quotval  25805  plydivlem4  25809  plydivex  25810  aalioulem2  25846  aalioulem5  25849  aalioulem6  25850  aaliou  25851  aaliou2  25853  aaliou2b  25854  isinag  28120  axcontlem7  28259  hashecclwwlkn1  29361  elunsn  31781  eliccioo  32128  tlt2  32170  prmidl  32589  mxidlval  32608  sibfof  33370  ballotlemfc0  33522  ballotlemfcc  33523  satfvsucsuc  34387  satf0op  34399  fmlafvel  34407  isfmlasuc  34410  satfv1fvfmla1  34445  seglelin  35119  lineunray  35150  topdifinfeq  36279  wl-ifp4impr  36396  mblfinlem2  36574  pridl  36953  maxidlval  36955  ispridlc  36986  pridlc  36987  dmnnzd  36991  lcfl7N  40420  aomclem8  41851  fzuntgd  42257  orbi1r  43319  iccpartgtl  46142  iccpartleu  46144  lindslinindsimp2lem5  47191  lindslinindsimp2  47192  rrx2pnedifcoorneorr  47451