Theorem orrd 861

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 850	. 2 ⊢ ((¬ 𝜓 → 𝜒) → (𝜓 ∨ 𝜒))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝜓 ∨ 𝜒))

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

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 206  df-or 846

This theorem is referenced by:  orc  865  olc  866  pm2.68  898  pm4.79  1001  19.30  1877  axi12  2698  r19.30  3113  r19.30OLD  3114  sspss  4108  eqoreldif  4696  pwpw0  4825  sssn  4838  unissint  4985  disjiund  5147  disjxiun  5153  otsndisj  5529  otiunsndisj  5530  pwssun  5581  isso2i  5633  ordtr3  6425  ordtri2or  6478  unizlim  6503  fvclss  7261  orduniorsuc  7847  ordzsl  7863  nn0suc  7915  xpexr  7939  soseq  8181  odi  8617  swoso  8776  erdisj  8796  ordtypelem7  9574  wemapsolem  9600  domwdom  9624  iscard3  10143  ackbij1lem18  10286  fin56  10443  entric  10607  gchdomtri  10679  inttsk  10824  r1tskina  10832  psslinpr  11081  ssxr  11340  letric  11371  mul0or  11911  mulge0b  12146  zeo  12710  uzm1  12922  xrletri  13196  supxrgtmnf  13372  sq01  14254  ruclem3  16256  prm2orodd  16713  phiprmpw  16799  pleval2i  18382  irredn0  20427  drngmul0orOLD  20761  lvecvs0or  21111  lssvs0or  21113  lspsnat  21148  lsppratlem1  21150  domnchr  21548  fctop  23021  cctop  23023  ppttop  23024  clslp  23166  restntr  23200  cnconn  23440  txindis  23652  txconn  23707  isufil2  23926  ufprim  23927  alexsubALTlem3  24067  pmltpc  25493  iundisj2  25592  limcco  25936  fta1b  26222  aalioulem2  26384  abelthlem2  26485  logreclem  26813  dchrfi  27307  2sqb  27484  nosepdmlem  27736  noetasuplem4  27789  sletric  27817  muls0ord  28209  tgbtwnconn1  28525  legov3  28548  coltr  28597  colline  28599  tglowdim2ln  28601  ragflat3  28656  ragperp  28667  lmieu  28734  lmicom  28738  lmimid  28744  numedglnl  29103  nvmul0or  30606  hvmul0or  30981  atomli  32338  atordi  32340  iundisj2f  32537  iundisj2fi  32728  chnind  32909  mxidlprm  33390  ssmxidl  33394  qsdrng  33417  zarclssn  33746  signsply0  34455  pthisspthorcycl  35023  cvmsdisj  35165  nepss  35607  dfon2lem6  35679  btwnconn1lem13  35990  wl-exeq  37296  eqvreldisj  38379  lsator0sp  38766  lkreqN  38935  2at0mat0  39291  trlator0  39937  dochkrshp4  41155  dochsat0  41223  lcfl6  41266  expeqidd  42105  rp-fakeimass  43270  frege124d  43519  clsk1independent  43804  mnringmulrcld  43993  pm10.57  44136  icccncfext  45598  fourierdlem70  45887  ichnreuop  47134  uzlidlring  47713  nneop  48015  mo0sn  48302