Theorem orrd 858

Description: Deduce disjunction from implication. (Contributed by NM, 27-Nov-1995.)

Hypothesis

Ref	Expression
orrd.1	⊢ (𝜑 → (¬ 𝜓 → 𝜒))

Assertion

Ref	Expression
orrd	⊢ (𝜑 → (𝜓 ∨ 𝜒))

Proof of Theorem orrd

Step	Hyp	Ref	Expression
1		orrd.1	. 2 ⊢ (𝜑 → (¬ 𝜓 → 𝜒))
2		pm2.54 847	. 2 ⊢ ((¬ 𝜓 → 𝜒) → (𝜓 ∨ 𝜒))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝜓 ∨ 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 842

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 208  df-or 843

This theorem is referenced by:  orc  862  olc  863  pm2.68  895  pm4.79  998  19.30  1867  axi12  2767  axi12OLD  2768  axbndOLD  2770  r19.30  3301  sspss  4003  eqoreldif  4535  pwpw0  4659  sssn  4672  pwsnALT  4744  unissint  4812  disjiund  4959  disjxiun  4965  otsndisj  5307  otiunsndisj  5308  pwssun  5351  isso2i  5403  ordtr3  6118  ordtri2or  6168  unizlim  6189  fvclss  6873  orduniorsuc  7408  ordzsl  7423  nn0suc  7469  xpexr  7486  odi  8062  swoso  8179  erdisj  8198  ordtypelem7  8841  wemapsolem  8867  domwdom  8891  iscard3  9372  ackbij1lem18  9512  fin56  9668  entric  9832  gchdomtri  9904  inttsk  10049  r1tskina  10057  psslinpr  10306  ssxr  10563  letric  10593  mul0or  11134  mulge0b  11364  zeo  11922  uzm1  12129  xrletri  12400  supxrgtmnf  12576  sq01  13440  ruclem3  15423  prm2orodd  15868  phiprmpw  15946  pleval2i  17407  irredn0  19147  drngmul0or  19217  lvecvs0or  19574  lssvs0or  19576  lspsnat  19611  lsppratlem1  19613  domnchr  20365  fctop  21300  cctop  21302  ppttop  21303  clslp  21444  restntr  21478  cnconn  21718  txindis  21930  txconn  21985  isufil2  22204  ufprim  22205  alexsubALTlem3  22345  pmltpc  23738  iundisj2  23837  limcco  24178  fta1b  24450  aalioulem2  24609  abelthlem2  24707  logreclem  25025  dchrfi  25517  2sqb  25694  tgbtwnconn1  26047  legov3  26070  coltr  26119  colline  26121  tglowdim2ln  26123  ragflat3  26178  ragperp  26189  lmieu  26256  lmicom  26260  lmimid  26266  numedglnl  26616  nvmul0or  28114  hvmul0or  28489  atomli  29846  atordi  29848  iundisj2f  30026  iundisj2fi  30202  signsply0  31434  pthisspthorcycl  31985  cvmsdisj  32127  nepss  32558  dfon2lem6  32643  soseq  32707  nosepdmlem  32798  noetalem3  32830  btwnconn1lem13  33171  wl-exeq  34327  eqvreldisj  35401  lsator0sp  35689  lkreqN  35858  2at0mat0  36213  trlator0  36859  dochkrshp4  38077  dochsat0  38145  lcfl6  38188  rp-fakeimass  39384  frege124d  39612  clsk1independent  39902  pm10.57  40262  icccncfext  41733  fourierdlem70  42025  ichnreuop  43138  uzlidlring  43700  nneop  44089