Theorem orbi2d 913

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∨ wo 844

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 210  df-or 845

This theorem is referenced by:  orbi1d  914  orbi12d  916  eueq2  3649  sbc2or  3729  r19.44zv  4407  rexprgf  4591  rextpg  4595  swopolem  5447  poleloe  5958  elsucg  6226  elsuc2g  6227  brdifun  8301  brwdom  9015  isfin1a  9703  elgch  10033  suplem2pr  10464  axlttri  10701  mulcan1g  11282  elznn0  11984  elznn  11985  zindd  12071  rpneg  12409  dfle2  12528  fzm1  12982  fzosplitsni  13143  hashv01gt1  13701  zeo5  15697  bitsf1  15785  lcmval  15926  lcmneg  15937  lcmass  15948  isprm6  16048  infpn2  16239  irredmul  19455  domneq0  20063  znfld  20252  quotval  24888  plydivlem4  24892  plydivex  24893  aalioulem2  24929  aalioulem5  24932  aalioulem6  24933  aaliou  24934  aaliou2  24936  aaliou2b  24937  isinag  26632  axcontlem7  26764  hashecclwwlkn1  27862  elunsn  30281  eliccioo  30633  tlt2  30677  prmidl  31023  mxidlval  31041  sibfof  31708  ballotlemfc0  31860  ballotlemfcc  31861  satfvsucsuc  32725  satf0op  32737  fmlafvel  32745  isfmlasuc  32748  satfv1fvfmla1  32783  seglelin  33690  lineunray  33721  topdifinfeq  34767  wl-ifp4impr  34884  mblfinlem2  35095  pridl  35475  maxidlval  35477  ispridlc  35508  pridlc  35509  dmnnzd  35513  lcfl7N  38797  aomclem8  40005  orbi1r  41216  iccpartgtl  43943  iccpartleu  43945  lindslinindsimp2lem5  44871  lindslinindsimp2  44872  rrx2pnedifcoorneorr  45131