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  3668  sbc2or  3748  r19.44zv  4465  elunsn  4644  rexprgf  4656  rextpg  4660  swopolem  5573  poleloe  6125  elsucg  6428  elsuc2g  6429  xpord2indlem  8145  brdifun  8727  brwdom  9539  isfin1a  10294  elgch  10631  suplem2pr  11062  axlttri  11305  mulcan1g  11891  elznn0  12630  elznn  12631  zindd  12722  rpneg  13076  dfle2  13198  fzm1  13662  fzosplitsni  13835  hashv01gt1  14409  zeo5  16446  bitsf1  16536  lcmval  16682  lcmneg  16693  lcmass  16704  isprm6  16805  infpn2  17005  irredmul  20570  lringuplu  20706  domneq0  20870  prmidl  21528  prmidlprop  21539  znfld  21773  quotval  26522  plydivlem4  26526  plydivex  26527  aalioulem2  26569  aalioulem5  26572  aalioulem6  26573  aaliou  26574  aaliou2  26576  aaliou2b  26577  elzs2  28664  elznns  28667  elplng  29137  plngcplem  29142  isinag  29236  brprlng  29295  axcontlem7  29427  hashecclwwlkn1  30547  eliccioo  33376  tlt2  33409  mxidlval  33864  rprmdvds  33929  sibfof  34851  ballotlemfc0  35004  ballotlemfcc  35005  satfvsucsuc  35944  satf0op  35956  fmlafvel  35964  isfmlasuc  35967  satfv1fvfmla1  36002  seglelin  36696  lineunray  36727  topdifinfeq  38104  wl-ifp4impr  38221  mblfinlem2  38407  pridl  38787  maxidlval  38789  ispridlc  38820  pridlc  38821  dmnnzd  38825  lcfl7N  42374  aomclem8  43902  fzuntgd  44298  orbi1r  45333  iccpartgtl  48326  iccpartleu  48328  nprmmul3  48429  clnbupgrel  48750  dfsclnbgr6  48774  idomnzd  49261  lindslinindsimp2lem5  49392  lindslinindsimp2  49393  rrx2pnedifcoorneorr  49647