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  3681  sbc2or  3762  r19.44zv  4467  elunsn  4647  rexprgf  4659  rextpg  4663  swopolem  5556  poleloe  6104  elsucg  6402  elsuc2g  6403  xpord2indlem  8126  brdifun  8701  brwdom  9520  isfin1a  10245  elgch  10575  suplem2pr  11006  axlttri  11245  mulcan1g  11831  elznn0  12544  elznn  12545  zindd  12635  rpneg  12985  dfle2  13107  fzm1  13568  fzosplitsni  13739  hashv01gt1  14310  zeo5  16326  bitsf1  16416  lcmval  16562  lcmneg  16573  lcmass  16584  isprm6  16684  infpn2  16884  irredmul  20338  lringuplu  20453  domneq0  20617  znfld  21470  quotval  26200  plydivlem4  26204  plydivex  26205  aalioulem2  26241  aalioulem5  26244  aalioulem6  26245  aaliou  26246  aaliou2  26248  aaliou2b  26249  elzs2  28287  elznns  28290  isinag  28765  axcontlem7  28897  hashecclwwlkn1  30006  eliccioo  32851  tlt2  32895  prmidl  33411  mxidlval  33432  rprmdvds  33490  sibfof  34331  ballotlemfc0  34484  ballotlemfcc  34485  satfvsucsuc  35352  satf0op  35364  fmlafvel  35372  isfmlasuc  35375  satfv1fvfmla1  35410  seglelin  36104  lineunray  36135  topdifinfeq  37338  wl-ifp4impr  37455  mblfinlem2  37652  pridl  38031  maxidlval  38033  ispridlc  38064  pridlc  38065  dmnnzd  38069  lcfl7N  41495  aomclem8  43050  fzuntgd  43447  orbi1r  44500  iccpartgtl  47427  iccpartleu  47429  clnbupgrel  47835  dfsclnbgr6  47858  lindslinindsimp2lem5  48451  lindslinindsimp2  48452  rrx2pnedifcoorneorr  48706