Theorem orbi2d 929

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  orbi1d  930  orbi12d  932  eueq2  3675  sbc2or  3755  r19.44zv  4472  elunsn  4651  rexprgf  4663  rextpg  4667  swopolem  5581  poleloe  6133  elsucg  6435  elsuc2g  6436  xpord2indlem  8145  brdifun  8727  brwdom  9532  isfin1a  10287  elgch  10618  suplem2pr  11049  axlttri  11292  mulcan1g  11878  elznn0  12617  elznn  12618  zindd  12709  rpneg  13062  dfle2  13184  fzm1  13648  fzosplitsni  13821  hashv01gt1  14395  zeo5  16432  bitsf1  16522  lcmval  16668  lcmneg  16679  lcmass  16690  isprm6  16791  infpn2  16991  irredmul  20537  lringuplu  20673  domneq0  20837  prmidl  21495  prmidlprop  21506  znfld  21740  quotval  26484  plydivlem4  26488  plydivex  26489  aalioulem2  26527  aalioulem5  26530  aalioulem6  26531  aaliou  26532  aaliou2  26534  aaliou2b  26535  elzs2  28623  elznns  28626  elplng  29093  plngcplem  29098  isinag  29186  brprlng  29219  axcontlem7  29351  hashecclwwlkn1  30471  eliccioo  33296  tlt2  33329  mxidlval  33784  rprmdvds  33849  sibfof  34771  ballotlemfc0  34924  ballotlemfcc  34925  satfvsucsuc  35870  satf0op  35882  fmlafvel  35890  isfmlasuc  35893  satfv1fvfmla1  35928  seglelin  36621  lineunray  36652  topdifinfeq  38029  wl-ifp4impr  38146  mblfinlem2  38342  pridl  38721  maxidlval  38723  ispridlc  38754  pridlc  38755  dmnnzd  38759  lcfl7N  42308  aomclem8  43821  fzuntgd  44217  orbi1r  45252  iccpartgtl  48208  iccpartleu  48210  nprmmul3  48311  clnbupgrel  48632  dfsclnbgr6  48656  idomnzd  49144  lindslinindsimp2lem5  49275  lindslinindsimp2  49276  rrx2pnedifcoorneorr  49530