Theorem orbi2d 738

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 382

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 197  df-or 384

This theorem is referenced by:  orbi1d  739  orbi12d  746  eueq2  3413  sbc2or  3477  r19.44zv  4102  rexprg  4267  rextpg  4269  swopolem  5073  poleloe  5562  elsucg  5830  elsuc2g  5831  brdifun  7816  brwdom  8513  isfin1a  9152  elgch  9482  suplem2pr  9913  axlttri  10147  mulcan1g  10718  elznn0  11430  elznn  11431  zindd  11516  rpneg  11901  dfle2  12018  fzm1  12458  fzosplitsni  12619  hashv01gt1  13173  zeo5  15127  bitsf1  15215  lcmval  15352  lcmneg  15363  lcmass  15374  isprm6  15473  infpn2  15664  irredmul  18755  domneq0  19345  znfld  19957  quotval  24092  plydivlem4  24096  plydivex  24097  aalioulem2  24133  aalioulem5  24136  aalioulem6  24137  aaliou  24138  aaliou2  24140  aaliou2b  24141  isinag  25774  axcontlem7  25895  hashecclwwlkn1  27041  eliccioo  29767  tlt2  29792  sibfof  30530  ballotlemfc0  30682  ballotlemfcc  30683  seglelin  32348  lineunray  32379  topdifinfeq  33328  mblfinlem2  33577  pridl  33966  maxidlval  33968  ispridlc  33999  pridlc  34000  dmnnzd  34004  lcfl7N  37107  aomclem8  37948  orbi1r  39033  iccpartgtl  41687  iccpartleu  41689  lindslinindsimp2lem5  42576  lindslinindsimp2  42577