Theorem orbi2d 915

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

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

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 848

This theorem is referenced by:  orbi1d  916  orbi12d  918  eueq2  3668  sbc2or  3749  r19.44zv  4462  elunsn  4640  rexprgf  4652  rextpg  4656  swopolem  5542  poleloe  6088  elsucg  6387  elsuc2g  6388  xpord2indlem  8089  brdifun  8665  brwdom  9472  isfin1a  10202  elgch  10533  suplem2pr  10964  axlttri  11204  mulcan1g  11790  elznn0  12503  elznn  12504  zindd  12593  rpneg  12939  dfle2  13061  fzm1  13523  fzosplitsni  13695  hashv01gt1  14268  zeo5  16283  bitsf1  16373  lcmval  16519  lcmneg  16530  lcmass  16541  isprm6  16641  infpn2  16841  irredmul  20365  lringuplu  20477  domneq0  20641  znfld  21515  quotval  26256  plydivlem4  26260  plydivex  26261  aalioulem2  26297  aalioulem5  26300  aalioulem6  26301  aaliou  26302  aaliou2  26304  aaliou2b  26305  elzs2  28395  elznns  28398  isinag  28910  axcontlem7  29043  hashecclwwlkn1  30152  eliccioo  33012  tlt2  33051  prmidl  33521  mxidlval  33542  rprmdvds  33600  sibfof  34497  ballotlemfc0  34650  ballotlemfcc  34651  satfvsucsuc  35559  satf0op  35571  fmlafvel  35579  isfmlasuc  35582  satfv1fvfmla1  35617  seglelin  36310  lineunray  36341  topdifinfeq  37555  wl-ifp4impr  37672  mblfinlem2  37859  pridl  38238  maxidlval  38240  ispridlc  38271  pridlc  38272  dmnnzd  38276  lcfl7N  41761  aomclem8  43303  fzuntgd  43699  orbi1r  44751  iccpartgtl  47672  iccpartleu  47674  clnbupgrel  48080  dfsclnbgr6  48104  lindslinindsimp2lem5  48708  lindslinindsimp2  48709  rrx2pnedifcoorneorr  48963