Theorem orbi2d 921

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∨ wo 853

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 208  df-or 854

This theorem is referenced by:  orbi1d  922  orbi12d  924  eueq2  3651  sbc2or  3732  r19.44zv  4437  elunsn  4615  rexprgf  4627  rextpg  4631  swopolem  5536  poleloe  6081  elsucg  6380  elsuc2g  6381  xpord2indlem  8087  brdifun  8664  brwdom  9472  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  20516  domneq0  20680  znfld  21535  quotval  26276  plydivlem4  26280  plydivex  26281  aalioulem2  26317  aalioulem5  26320  aalioulem6  26321  aaliou  26322  aaliou2  26324  aaliou2b  26325  elzs2  28409  elznns  28412  isinag  28924  axcontlem7  29057  hashecclwwlkn1  30165  eliccioo  33009  tlt2  33048  prmidl  33523  mxidlval  33544  rprmdvds  33602  sibfof  34524  ballotlemfc0  34677  ballotlemfcc  34678  satfvsucsuc  35593  satf0op  35605  fmlafvel  35613  isfmlasuc  35616  satfv1fvfmla1  35651  seglelin  36344  lineunray  36375  topdifinfeq  37712  wl-ifp4impr  37829  mblfinlem2  38025  pridl  38404  maxidlval  38406  ispridlc  38437  pridlc  38438  dmnnzd  38442  lcfl7N  41993  aomclem8  43506  fzuntgd  43902  orbi1r  44954  iccpartgtl  47901  iccpartleu  47903  nprmmul3  48004  clnbupgrel  48325  dfsclnbgr6  48349  lindslinindsimp2lem5  48953  lindslinindsimp2  48954  rrx2pnedifcoorneorr  49208