Theorem orbi2d 928

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∨ wo 860

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 210  df-or 861

This theorem is referenced by:  orbi1d  929  orbi12d  931  eueq2  3673  sbc2or  3753  r19.44zv  4470  elunsn  4649  rexprgf  4661  rextpg  4665  swopolem  5579  poleloe  6131  elsucg  6431  elsuc2g  6432  xpord2indlem  8139  brdifun  8721  brwdom  9525  isfin1a  10271  elgch  10602  suplem2pr  11033  axlttri  11276  mulcan1g  11862  elznn0  12601  elznn  12602  zindd  12692  rpneg  13045  dfle2  13167  fzm1  13631  fzosplitsni  13804  hashv01gt1  14377  zeo5  16409  bitsf1  16499  lcmval  16645  lcmneg  16656  lcmass  16667  isprm6  16768  infpn2  16968  irredmul  20507  lringuplu  20643  domneq0  20807  prmidl  21465  prmidlprop  21476  znfld  21710  quotval  26453  plydivlem4  26457  plydivex  26458  aalioulem2  26496  aalioulem5  26499  aalioulem6  26500  aaliou  26501  aaliou2  26503  aaliou2b  26504  elzs2  28592  elznns  28595  elplng  29062  plngcplem  29067  isinag  29155  brprlng  29188  axcontlem7  29320  hashecclwwlkn1  30428  eliccioo  33250  tlt2  33289  mxidlval  33744  rprmdvds  33809  sibfof  34730  ballotlemfc0  34883  ballotlemfcc  34884  satfvsucsuc  35857  satf0op  35869  fmlafvel  35877  isfmlasuc  35880  satfv1fvfmla1  35915  seglelin  36608  lineunray  36639  topdifinfeq  37996  wl-ifp4impr  38113  mblfinlem2  38309  pridl  38688  maxidlval  38690  ispridlc  38721  pridlc  38722  dmnnzd  38726  lcfl7N  42275  aomclem8  43788  fzuntgd  44184  orbi1r  45219  iccpartgtl  48175  iccpartleu  48177  nprmmul3  48278  clnbupgrel  48599  dfsclnbgr6  48623  idomnzd  49111  lindslinindsimp2lem5  49242  lindslinindsimp2  49243  rrx2pnedifcoorneorr  49497