Theorem orbi2d 916

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∨ wo 848

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 849

This theorem is referenced by:  orbi1d  917  orbi12d  919  eueq2  3657  sbc2or  3738  r19.44zv  4450  elunsn  4628  rexprgf  4640  rextpg  4644  swopolem  5542  poleloe  6088  elsucg  6387  elsuc2g  6388  xpord2indlem  8090  brdifun  8667  brwdom  9475  isfin1a  10205  elgch  10536  suplem2pr  10967  axlttri  11208  mulcan1g  11794  elznn0  12530  elznn  12531  zindd  12621  rpneg  12967  dfle2  13089  fzm1  13552  fzosplitsni  13725  hashv01gt1  14298  zeo5  16316  bitsf1  16406  lcmval  16552  lcmneg  16563  lcmass  16574  isprm6  16675  infpn2  16875  irredmul  20400  lringuplu  20512  domneq0  20676  znfld  21550  quotval  26269  plydivlem4  26273  plydivex  26274  aalioulem2  26310  aalioulem5  26313  aalioulem6  26314  aaliou  26315  aaliou2  26317  aaliou2b  26318  elzs2  28405  elznns  28408  isinag  28920  axcontlem7  29053  hashecclwwlkn1  30162  eliccioo  33005  tlt2  33044  prmidl  33515  mxidlval  33536  rprmdvds  33594  sibfof  34500  ballotlemfc0  34653  ballotlemfcc  34654  satfvsucsuc  35563  satf0op  35575  fmlafvel  35583  isfmlasuc  35586  satfv1fvfmla1  35621  seglelin  36314  lineunray  36345  topdifinfeq  37680  wl-ifp4impr  37797  mblfinlem2  37993  pridl  38372  maxidlval  38374  ispridlc  38405  pridlc  38406  dmnnzd  38410  lcfl7N  41961  aomclem8  43507  fzuntgd  43903  orbi1r  44955  iccpartgtl  47898  iccpartleu  47900  nprmmul3  48001  clnbupgrel  48322  dfsclnbgr6  48346  lindslinindsimp2lem5  48950  lindslinindsimp2  48951  rrx2pnedifcoorneorr  49205