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  3678  sbc2or  3759  r19.44zv  4463  elunsn  4643  rexprgf  4655  rextpg  4659  swopolem  5549  poleloe  6092  elsucg  6390  elsuc2g  6391  xpord2indlem  8103  brdifun  8678  brwdom  9496  isfin1a  10221  elgch  10551  suplem2pr  10982  axlttri  11221  mulcan1g  11807  elznn0  12520  elznn  12521  zindd  12611  rpneg  12961  dfle2  13083  fzm1  13544  fzosplitsni  13715  hashv01gt1  14286  zeo5  16302  bitsf1  16392  lcmval  16538  lcmneg  16549  lcmass  16560  isprm6  16660  infpn2  16860  irredmul  20314  lringuplu  20429  domneq0  20593  znfld  21446  quotval  26176  plydivlem4  26180  plydivex  26181  aalioulem2  26217  aalioulem5  26220  aalioulem6  26221  aaliou  26222  aaliou2  26224  aaliou2b  26225  elzs2  28263  elznns  28266  isinag  28741  axcontlem7  28873  hashecclwwlkn1  29979  eliccioo  32824  tlt2  32868  prmidl  33384  mxidlval  33405  rprmdvds  33463  sibfof  34304  ballotlemfc0  34457  ballotlemfcc  34458  satfvsucsuc  35325  satf0op  35337  fmlafvel  35345  isfmlasuc  35348  satfv1fvfmla1  35383  seglelin  36077  lineunray  36108  topdifinfeq  37311  wl-ifp4impr  37428  mblfinlem2  37625  pridl  38004  maxidlval  38006  ispridlc  38037  pridlc  38038  dmnnzd  38042  lcfl7N  41468  aomclem8  43023  fzuntgd  43420  orbi1r  44473  iccpartgtl  47400  iccpartleu  47402  clnbupgrel  47808  dfsclnbgr6  47831  lindslinindsimp2lem5  48424  lindslinindsimp2  48425  rrx2pnedifcoorneorr  48679