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  3672  sbc2or  3753  r19.44zv  4457  elunsn  4637  rexprgf  4649  rextpg  4653  swopolem  5541  poleloe  6084  elsucg  6381  elsuc2g  6382  xpord2indlem  8087  brdifun  8662  brwdom  9478  isfin1a  10205  elgch  10535  suplem2pr  10966  axlttri  11206  mulcan1g  11792  elznn0  12505  elznn  12506  zindd  12596  rpneg  12946  dfle2  13068  fzm1  13529  fzosplitsni  13700  hashv01gt1  14271  zeo5  16286  bitsf1  16376  lcmval  16522  lcmneg  16533  lcmass  16544  isprm6  16644  infpn2  16844  irredmul  20333  lringuplu  20448  domneq0  20612  znfld  21486  quotval  26217  plydivlem4  26221  plydivex  26222  aalioulem2  26258  aalioulem5  26261  aalioulem6  26262  aaliou  26263  aaliou2  26265  aaliou2b  26266  elzs2  28311  elznns  28314  isinag  28802  axcontlem7  28934  hashecclwwlkn1  30040  eliccioo  32890  tlt2  32930  prmidl  33396  mxidlval  33417  rprmdvds  33475  sibfof  34327  ballotlemfc0  34480  ballotlemfcc  34481  satfvsucsuc  35357  satf0op  35369  fmlafvel  35377  isfmlasuc  35380  satfv1fvfmla1  35415  seglelin  36109  lineunray  36140  topdifinfeq  37343  wl-ifp4impr  37460  mblfinlem2  37657  pridl  38036  maxidlval  38038  ispridlc  38069  pridlc  38070  dmnnzd  38074  lcfl7N  41500  aomclem8  43054  fzuntgd  43451  orbi1r  44504  iccpartgtl  47430  iccpartleu  47432  clnbupgrel  47838  dfsclnbgr6  47862  lindslinindsimp2lem5  48467  lindslinindsimp2  48468  rrx2pnedifcoorneorr  48722