Theorem orbi2d 912

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

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

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 844

This theorem is referenced by:  orbi1d  913  orbi12d  915  eueq2  3648  sbc2or  3728  r19.44zv  4439  rexprgf  4634  rextpg  4640  swopolem  5512  poleloe  6033  elsucg  6330  elsuc2g  6331  brdifun  8501  brwdom  9287  isfin1a  10032  elgch  10362  suplem2pr  10793  axlttri  11030  mulcan1g  11611  elznn0  12317  elznn  12318  zindd  12404  rpneg  12744  dfle2  12863  fzm1  13318  fzosplitsni  13479  hashv01gt1  14040  zeo5  16046  bitsf1  16134  lcmval  16278  lcmneg  16289  lcmass  16300  isprm6  16400  infpn2  16595  irredmul  19932  domneq0  20549  znfld  20749  quotval  25433  plydivlem4  25437  plydivex  25438  aalioulem2  25474  aalioulem5  25477  aalioulem6  25478  aaliou  25479  aaliou2  25481  aaliou2b  25482  isinag  27180  axcontlem7  27319  hashecclwwlkn1  28420  elunsn  30837  eliccioo  31184  tlt2  31226  prmidl  31594  mxidlval  31612  sibfof  32286  ballotlemfc0  32438  ballotlemfcc  32439  satfvsucsuc  33306  satf0op  33318  fmlafvel  33326  isfmlasuc  33329  satfv1fvfmla1  33364  xpord2ind  33773  seglelin  34397  lineunray  34428  topdifinfeq  35500  wl-ifp4impr  35617  mblfinlem2  35794  pridl  36174  maxidlval  36176  ispridlc  36207  pridlc  36208  dmnnzd  36212  lcfl7N  39494  aomclem8  40866  orbi1r  42083  iccpartgtl  44830  iccpartleu  44832  lindslinindsimp2lem5  45755  lindslinindsimp2  45756  rrx2pnedifcoorneorr  46015