Theorem orbi2d 914

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∨ wo 845

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 846

This theorem is referenced by:  orbi1d  915  orbi12d  917  eueq2  3671  sbc2or  3751  r19.44zv  4466  rexprgf  4659  rextpg  4665  swopolem  5560  poleloe  6090  elsucg  6390  elsuc2g  6391  xpord2indlem  8084  brdifun  8684  brwdom  9512  isfin1a  10237  elgch  10567  suplem2pr  10998  axlttri  11235  mulcan1g  11817  elznn0  12523  elznn  12524  zindd  12613  rpneg  12956  dfle2  13076  fzm1  13531  fzosplitsni  13693  hashv01gt1  14255  zeo5  16249  bitsf1  16337  lcmval  16479  lcmneg  16490  lcmass  16501  isprm6  16601  infpn2  16796  irredmul  20154  lringuplu  20224  domneq0  20804  znfld  21004  quotval  25689  plydivlem4  25693  plydivex  25694  aalioulem2  25730  aalioulem5  25733  aalioulem6  25734  aaliou  25735  aaliou2  25737  aaliou2b  25738  isinag  27843  axcontlem7  27982  hashecclwwlkn1  29084  elunsn  31503  eliccioo  31857  tlt2  31899  prmidl  32288  mxidlval  32306  sibfof  33029  ballotlemfc0  33181  ballotlemfcc  33182  satfvsucsuc  34046  satf0op  34058  fmlafvel  34066  isfmlasuc  34069  satfv1fvfmla1  34104  seglelin  34777  lineunray  34808  topdifinfeq  35894  wl-ifp4impr  36011  mblfinlem2  36189  pridl  36569  maxidlval  36571  ispridlc  36602  pridlc  36603  dmnnzd  36607  lcfl7N  40037  aomclem8  41446  fzuntgd  41852  orbi1r  42914  iccpartgtl  45738  iccpartleu  45740  lindslinindsimp2lem5  46663  lindslinindsimp2  46664  rrx2pnedifcoorneorr  46923