Theorem orrd 863

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

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

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 207  df-or 848

This theorem is referenced by:  orc  867  olc  868  pm2.68  900  pm4.79  1005  19.30  1881  axi12  2700  r19.30  3101  sspss  4068  eqoreldif  4652  pwpw0  4780  sssn  4793  unissint  4939  disjiund  5101  disjxiun  5107  otsndisj  5482  otiunsndisj  5483  pwssun  5533  isso2i  5586  ordtr3  6381  ordtri2or  6435  unizlim  6460  fvclss  7218  orduniorsuc  7808  ordzsl  7824  nn0suc  7873  xpexr  7897  soseq  8141  odi  8546  swoso  8708  erdisj  8731  ordtypelem7  9484  wemapsolem  9510  domwdom  9534  iscard3  10053  ackbij1lem18  10196  fin56  10353  entric  10517  gchdomtri  10589  inttsk  10734  r1tskina  10742  psslinpr  10991  1re  11181  ssxr  11250  letric  11281  mul0or  11825  mulge0b  12060  zeo  12627  uzm1  12838  xrletri  13120  supxrgtmnf  13296  sq01  14197  ruclem3  16208  prm2orodd  16668  phiprmpw  16753  pleval2i  18302  irredn0  20339  drngmul0orOLD  20677  lvecvs0or  21025  lssvs0or  21027  lspsnat  21062  lsppratlem1  21064  domnchr  21449  fctop  22898  cctop  22900  ppttop  22901  clslp  23042  restntr  23076  cnconn  23316  txindis  23528  txconn  23583  isufil2  23802  ufprim  23803  alexsubALTlem3  23943  pmltpc  25358  iundisj2  25457  limcco  25801  fta1b  26084  aalioulem2  26248  abelthlem2  26349  logreclem  26679  dchrfi  27173  2sqb  27350  nosepdmlem  27602  noetasuplem4  27655  sletric  27683  muls0ord  28095  tgbtwnconn1  28509  legov3  28532  coltr  28581  colline  28583  tglowdim2ln  28585  ragflat3  28640  ragperp  28651  lmieu  28718  lmicom  28722  lmimid  28728  numedglnl  29078  pthisspthorcycl  29739  nvmul0or  30586  hvmul0or  30961  atomli  32318  atordi  32320  iundisj2f  32526  iundisj2fi  32727  chnind  32944  gsumfs2d  33002  mxidlprm  33448  ssmxidl  33452  qsdrng  33475  zarclssn  33870  signsply0  34549  cvmsdisj  35264  nepss  35712  dfon2lem6  35783  btwnconn1lem13  36094  wl-exeq  37529  eqvreldisj  38612  lsator0sp  39001  lkreqN  39170  2at0mat0  39526  trlator0  40172  dochkrshp4  41390  dochsat0  41458  lcfl6  41501  expeqidd  42320  sn-remul0ord  42403  rp-fakeimass  43508  frege124d  43757  clsk1independent  44042  mnringmulrcld  44224  pm10.57  44367  icccncfext  45892  fourierdlem70  46181  ichnreuop  47477  uzlidlring  48227  nneop  48519  mo0sn  48808  euendfunc2  49520