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

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

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 847

This theorem is referenced by:  orbi1d  916  orbi12d  918  eueq2  3609  sbc2or  3689  r19.44zv  4390  rexprgf  4584  rextpg  4590  swopolem  5452  poleloe  5965  elsucg  6239  elsuc2g  6240  brdifun  8349  brwdom  9104  isfin1a  9792  elgch  10122  suplem2pr  10553  axlttri  10790  mulcan1g  11371  elznn0  12077  elznn  12078  zindd  12164  rpneg  12504  dfle2  12623  fzm1  13078  fzosplitsni  13239  hashv01gt1  13797  zeo5  15801  bitsf1  15889  lcmval  16033  lcmneg  16044  lcmass  16055  isprm6  16155  infpn2  16349  irredmul  19581  domneq0  20189  znfld  20379  quotval  25040  plydivlem4  25044  plydivex  25045  aalioulem2  25081  aalioulem5  25084  aalioulem6  25085  aaliou  25086  aaliou2  25088  aaliou2b  25089  isinag  26784  axcontlem7  26916  hashecclwwlkn1  28014  elunsn  30432  eliccioo  30780  tlt2  30824  prmidl  31187  mxidlval  31205  sibfof  31877  ballotlemfc0  32029  ballotlemfcc  32030  satfvsucsuc  32898  satf0op  32910  fmlafvel  32918  isfmlasuc  32921  satfv1fvfmla1  32956  xpord2ind  33405  seglelin  34056  lineunray  34087  topdifinfeq  35144  wl-ifp4impr  35261  mblfinlem2  35438  pridl  35818  maxidlval  35820  ispridlc  35851  pridlc  35852  dmnnzd  35856  lcfl7N  39138  aomclem8  40458  orbi1r  41668  iccpartgtl  44412  iccpartleu  44414  lindslinindsimp2lem5  45337  lindslinindsimp2  45338  rrx2pnedifcoorneorr  45597