Theorem orrd 864

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

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

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 849

This theorem is referenced by:  orc  868  olc  869  pm2.68  901  pm4.79  1006  19.30  1883  axi12  2707  r19.30  3105  sspss  4056  eqoreldif  4644  pwpw0  4771  sssn  4784  unissint  4929  disjiund  5091  disjxiun  5097  otsndisj  5475  otiunsndisj  5476  pwssun  5524  isso2i  5577  ordtr3  6371  ordtri2or  6425  unizlim  6449  fvclss  7197  orduniorsuc  7782  ordzsl  7797  nn0suc  7846  xpexr  7870  soseq  8111  odi  8516  swoso  8680  erdisj  8703  ordtypelem7  9441  wemapsolem  9467  domwdom  9491  iscard3  10015  ackbij1lem18  10158  fin56  10315  entric  10479  gchdomtri  10552  inttsk  10697  r1tskina  10705  psslinpr  10954  1re  11144  ssxr  11214  letric  11245  mul0or  11789  mulge0b  12024  zeo  12590  uzm1  12797  xrletri  13079  supxrgtmnf  13256  sq01  14160  ruclem3  16170  prm2orodd  16630  phiprmpw  16715  pleval2i  18269  chnind  18556  irredn0  20371  drngmul0orOLD  20706  lvecvs0or  21075  lssvs0or  21077  lspsnat  21112  lsppratlem1  21114  domnchr  21499  fctop  22960  cctop  22962  ppttop  22963  clslp  23104  restntr  23138  cnconn  23378  txindis  23590  txconn  23645  isufil2  23864  ufprim  23865  alexsubALTlem3  24005  pmltpc  25419  iundisj2  25518  limcco  25862  fta1b  26145  aalioulem2  26309  abelthlem2  26410  logreclem  26740  dchrfi  27234  2sqb  27411  nosepdmlem  27663  noetasuplem4  27716  lestric  27748  muls0ord  28193  bdayfinbndlem1  28475  tgbtwnconn1  28659  legov3  28682  coltr  28731  colline  28733  tglowdim2ln  28735  ragflat3  28790  ragperp  28801  lmieu  28868  lmicom  28872  lmimid  28878  numedglnl  29229  pthisspthorcycl  29887  nvmul0or  30737  hvmul0or  31112  atomli  32469  atordi  32471  iundisj2f  32676  iundisj2fi  32887  gsumfs2d  33154  mxidlprm  33562  ssmxidl  33566  qsdrng  33589  zarclssn  34050  signsply0  34728  cvmsdisj  35483  nepss  35931  dfon2lem6  35999  btwnconn1lem13  36312  wl-exeq  37786  eqvreldisj  38946  lsator0sp  39374  lkreqN  39543  2at0mat0  39898  trlator0  40544  dochkrshp4  41762  dochsat0  41830  lcfl6  41873  expeqidd  42692  sn-remul0ord  42775  rp-fakeimass  43865  frege124d  44114  clsk1independent  44399  mnringmulrcld  44581  pm10.57  44724  icccncfext  46242  fourierdlem70  46531  ichnreuop  47829  uzlidlring  48592  nneop  48883  mo0sn  49172  euendfunc2  49883