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

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

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 385

This theorem is referenced by:  orbi1d  739  orbi12d  746  eueq2  3380  sbc2or  3444  r19.44zv  4069  rexprg  4235  rextpg  4237  swopolem  5044  poleloe  5527  elsucg  5792  elsuc2g  5793  brdifun  7771  brwdom  8472  isfin1a  9114  elgch  9444  suplem2pr  9875  axlttri  10109  mulcan1g  10680  elznn0  11392  elznn  11393  zindd  11478  rpneg  11863  dfle2  11980  fzm1  12420  fzosplitsni  12579  hashv01gt1  13133  zeo5  15080  bitsf1  15168  lcmval  15305  lcmneg  15316  lcmass  15327  isprm6  15426  infpn2  15617  irredmul  18709  domneq0  19297  znfld  19909  quotval  24047  plydivlem4  24051  plydivex  24052  aalioulem2  24088  aalioulem5  24091  aalioulem6  24092  aaliou  24093  aaliou2  24095  aaliou2b  24096  isinag  25729  axcontlem7  25850  hashecclwwlksn1  26954  eliccioo  29639  tlt2  29664  sibfof  30402  ballotlemfc0  30554  ballotlemfcc  30555  seglelin  32223  lineunray  32254  topdifinfeq  33198  mblfinlem2  33447  pridl  33836  maxidlval  33838  ispridlc  33869  pridlc  33870  dmnnzd  33874  lcfl7N  36790  aomclem8  37631  orbi1r  38716  iccpartgtl  41362  iccpartleu  41364  lindslinindsimp2lem5  42251  lindslinindsimp2  42252