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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∨ 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 209  df-or 844

This theorem is referenced by:  orbi1d  913  orbi12d  915  eueq2  3703  sbc2or  3783  r19.44zv  4451  rexprgf  4633  rextpg  4637  swopolem  5485  poleloe  5993  elsucg  6260  elsuc2g  6261  brdifun  8320  brwdom  9033  isfin1a  9716  elgch  10046  suplem2pr  10477  axlttri  10714  mulcan1g  11295  elznn0  11999  elznn  12000  zindd  12086  rpneg  12424  dfle2  12543  fzm1  12990  fzosplitsni  13151  hashv01gt1  13708  zeo5  15707  bitsf1  15797  lcmval  15938  lcmneg  15949  lcmass  15960  isprm6  16060  infpn2  16251  irredmul  19461  domneq0  20072  znfld  20709  quotval  24883  plydivlem4  24887  plydivex  24888  aalioulem2  24924  aalioulem5  24927  aalioulem6  24928  aaliou  24929  aaliou2  24931  aaliou2b  24932  isinag  26626  axcontlem7  26758  hashecclwwlkn1  27858  elunsn  30275  eliccioo  30609  tlt2  30653  prmidl  30959  mxidlval  30972  sibfof  31600  ballotlemfc0  31752  ballotlemfcc  31753  satfvsucsuc  32614  satf0op  32626  fmlafvel  32634  isfmlasuc  32637  satfv1fvfmla1  32672  seglelin  33579  lineunray  33610  topdifinfeq  34633  mblfinlem2  34932  pridl  35317  maxidlval  35319  ispridlc  35350  pridlc  35351  dmnnzd  35355  lcfl7N  38639  aomclem8  39668  orbi1r  40851  iccpartgtl  43593  iccpartleu  43595  lindslinindsimp2lem5  44524  lindslinindsimp2  44525  rrx2pnedifcoorneorr  44711