Theorem orbi2d 914

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∨ wo 845

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 206  df-or 846

This theorem is referenced by:  orbi1d  915  orbi12d  917  eueq2  3650  sbc2or  3730  r19.44zv  4440  rexprgf  4633  rextpg  4639  swopolem  5524  poleloe  6051  elsucg  6348  elsuc2g  6349  brdifun  8558  brwdom  9370  isfin1a  10094  elgch  10424  suplem2pr  10855  axlttri  11092  mulcan1g  11674  elznn0  12380  elznn  12381  zindd  12467  rpneg  12808  dfle2  12927  fzm1  13382  fzosplitsni  13544  hashv01gt1  14105  zeo5  16110  bitsf1  16198  lcmval  16342  lcmneg  16353  lcmass  16364  isprm6  16464  infpn2  16659  irredmul  19996  domneq0  20613  znfld  20813  quotval  25497  plydivlem4  25501  plydivex  25502  aalioulem2  25538  aalioulem5  25541  aalioulem6  25542  aaliou  25543  aaliou2  25545  aaliou2b  25546  isinag  27244  axcontlem7  27383  hashecclwwlkn1  28486  elunsn  30903  eliccioo  31250  tlt2  31292  prmidl  31660  mxidlval  31678  sibfof  32352  ballotlemfc0  32504  ballotlemfcc  32505  satfvsucsuc  33372  satf0op  33384  fmlafvel  33392  isfmlasuc  33395  satfv1fvfmla1  33430  xpord2ind  33839  seglelin  34463  lineunray  34494  topdifinfeq  35565  wl-ifp4impr  35682  mblfinlem2  35859  pridl  36239  maxidlval  36241  ispridlc  36272  pridlc  36273  dmnnzd  36277  lcfl7N  39557  aomclem8  40924  fzuntgd  41103  orbi1r  42168  iccpartgtl  44936  iccpartleu  44938  lindslinindsimp2lem5  45861  lindslinindsimp2  45862  rrx2pnedifcoorneorr  46121