Theorem orbi2d 940

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∨ wo 874

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 199  df-or 875

This theorem is referenced by:  orbi1d  941  orbi12d  943  eueq2  3576  sbc2or  3642  r19.44zv  4262  rexprg  4425  rextpg  4427  swopolem  5242  poleloe  5745  elsucg  6008  elsuc2g  6009  brdifun  8011  brwdom  8714  isfin1a  9402  elgch  9732  suplem2pr  10163  axlttri  10399  mulcan1g  10972  elznn0  11681  elznn  11682  zindd  11768  rpneg  12108  dfle2  12227  fzm1  12674  fzosplitsni  12834  hashv01gt1  13385  zeo5  15416  bitsf1  15503  lcmval  15640  lcmneg  15651  lcmass  15662  isprm6  15759  infpn2  15950  irredmul  19025  domneq0  19620  znfld  20230  quotval  24388  plydivlem4  24392  plydivex  24393  aalioulem2  24429  aalioulem5  24432  aalioulem6  24433  aaliou  24434  aaliou2  24436  aaliou2b  24437  isinag  26085  axcontlem7  26207  hashecclwwlkn1  27395  eliccioo  30155  tlt2  30180  sibfof  30918  ballotlemfc0  31071  ballotlemfcc  31072  seglelin  32736  lineunray  32767  topdifinfeq  33696  mblfinlem2  33936  pridl  34323  maxidlval  34325  ispridlc  34356  pridlc  34357  dmnnzd  34361  lcfl7N  37522  aomclem8  38416  orbi1r  39496  iccpartgtl  42202  iccpartleu  42204  lindslinindsimp2lem5  43050  lindslinindsimp2  43051