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  28089  axcontlem7  28228  hashecclwwlkn1  29330  elunsn  31750  eliccioo  32097  tlt2  32139  prmidl  32558  mxidlval  32577  sibfof  33339  ballotlemfc0  33491  ballotlemfcc  33492  satfvsucsuc  34356  satf0op  34368  fmlafvel  34376  isfmlasuc  34379  satfv1fvfmla1  34414  seglelin  35088  lineunray  35119  topdifinfeq  36231  wl-ifp4impr  36348  mblfinlem2  36526  pridl  36905  maxidlval  36907  ispridlc  36938  pridlc  36939  dmnnzd  36943  lcfl7N  40372  aomclem8  41803  fzuntgd  42209  orbi1r  43271  iccpartgtl  46094  iccpartleu  46096  lindslinindsimp2lem5  47143  lindslinindsimp2  47144  rrx2pnedifcoorneorr  47403