Theorem orbi2d 916

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

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

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 849

This theorem is referenced by:  orbi1d  917  orbi12d  919  eueq2  3716  sbc2or  3797  r19.44zv  4504  elunsn  4683  rexprgf  4695  rextpg  4699  swopolem  5602  poleloe  6151  elsucg  6452  elsuc2g  6453  xpord2indlem  8172  brdifun  8775  brwdom  9607  isfin1a  10332  elgch  10662  suplem2pr  11093  axlttri  11332  mulcan1g  11916  elznn0  12628  elznn  12629  zindd  12719  rpneg  13067  dfle2  13189  fzm1  13647  fzosplitsni  13817  hashv01gt1  14384  zeo5  16393  bitsf1  16483  lcmval  16629  lcmneg  16640  lcmass  16651  isprm6  16751  infpn2  16951  irredmul  20429  lringuplu  20544  domneq0  20708  znfld  21579  quotval  26334  plydivlem4  26338  plydivex  26339  aalioulem2  26375  aalioulem5  26378  aalioulem6  26379  aaliou  26380  aaliou2  26382  aaliou2b  26383  elzs2  28385  elznns  28388  isinag  28846  axcontlem7  28985  hashecclwwlkn1  30096  eliccioo  32913  tlt2  32959  prmidl  33468  mxidlval  33489  rprmdvds  33547  sibfof  34342  ballotlemfc0  34495  ballotlemfcc  34496  satfvsucsuc  35370  satf0op  35382  fmlafvel  35390  isfmlasuc  35393  satfv1fvfmla1  35428  seglelin  36117  lineunray  36148  topdifinfeq  37351  wl-ifp4impr  37468  mblfinlem2  37665  pridl  38044  maxidlval  38046  ispridlc  38077  pridlc  38078  dmnnzd  38082  lcfl7N  41503  aomclem8  43073  fzuntgd  43471  orbi1r  44530  iccpartgtl  47413  iccpartleu  47415  clnbupgrel  47821  dfsclnbgr6  47844  lindslinindsimp2lem5  48379  lindslinindsimp2  48380  rrx2pnedifcoorneorr  48638