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  1882  axi12  2703  r19.30  3100  sspss  4051  eqoreldif  4637  pwpw0  4764  sssn  4777  unissint  4922  disjiund  5084  disjxiun  5090  otsndisj  5462  otiunsndisj  5463  pwssun  5511  isso2i  5564  ordtr3  6357  ordtri2or  6411  unizlim  6435  fvclss  7181  orduniorsuc  7766  ordzsl  7781  nn0suc  7830  xpexr  7854  soseq  8095  odi  8500  swoso  8662  erdisj  8685  ordtypelem7  9417  wemapsolem  9443  domwdom  9467  iscard3  9991  ackbij1lem18  10134  fin56  10291  entric  10455  gchdomtri  10527  inttsk  10672  r1tskina  10680  psslinpr  10929  1re  11119  ssxr  11189  letric  11220  mul0or  11764  mulge0b  11999  zeo  12565  uzm1  12772  xrletri  13054  supxrgtmnf  13230  sq01  14134  ruclem3  16144  prm2orodd  16604  phiprmpw  16689  pleval2i  18242  chnind  18529  irredn0  20343  drngmul0orOLD  20678  lvecvs0or  21047  lssvs0or  21049  lspsnat  21084  lsppratlem1  21086  domnchr  21471  fctop  22920  cctop  22922  ppttop  22923  clslp  23064  restntr  23098  cnconn  23338  txindis  23550  txconn  23605  isufil2  23824  ufprim  23825  alexsubALTlem3  23965  pmltpc  25379  iundisj2  25478  limcco  25822  fta1b  26105  aalioulem2  26269  abelthlem2  26370  logreclem  26700  dchrfi  27194  2sqb  27371  nosepdmlem  27623  noetasuplem4  27676  sletric  27704  muls0ord  28125  tgbtwnconn1  28554  legov3  28577  coltr  28626  colline  28628  tglowdim2ln  28630  ragflat3  28685  ragperp  28696  lmieu  28763  lmicom  28767  lmimid  28773  numedglnl  29124  pthisspthorcycl  29782  nvmul0or  30632  hvmul0or  31007  atomli  32364  atordi  32366  iundisj2f  32572  iundisj2fi  32784  gsumfs2d  33042  mxidlprm  33442  ssmxidl  33446  qsdrng  33469  zarclssn  33907  signsply0  34585  cvmsdisj  35335  nepss  35783  dfon2lem6  35851  btwnconn1lem13  36164  wl-exeq  37599  eqvreldisj  38731  lsator0sp  39121  lkreqN  39290  2at0mat0  39645  trlator0  40291  dochkrshp4  41509  dochsat0  41577  lcfl6  41620  expeqidd  42444  sn-remul0ord  42527  rp-fakeimass  43630  frege124d  43879  clsk1independent  44164  mnringmulrcld  44346  pm10.57  44489  icccncfext  46010  fourierdlem70  46299  ichnreuop  47597  uzlidlring  48360  nneop  48652  mo0sn  48941  euendfunc2  49653