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  4043  eqoreldif  4630  pwpw0  4757  sssn  4770  unissint  4915  disjiund  5077  disjxiun  5083  otsndisj  5467  otiunsndisj  5468  pwssun  5516  isso2i  5569  ordtr3  6363  ordtri2or  6417  unizlim  6441  fvclss  7189  orduniorsuc  7774  ordzsl  7789  nn0suc  7838  xpexr  7862  soseq  8102  odi  8507  swoso  8671  erdisj  8694  ordtypelem7  9432  wemapsolem  9458  domwdom  9482  iscard3  10006  ackbij1lem18  10149  fin56  10306  entric  10470  gchdomtri  10543  inttsk  10688  r1tskina  10696  psslinpr  10945  1re  11135  ssxr  11206  letric  11237  mul0or  11781  mulge0b  12017  zeo  12606  uzm1  12813  xrletri  13095  supxrgtmnf  13272  sq01  14178  ruclem3  16191  prm2orodd  16651  phiprmpw  16737  pleval2i  18291  chnind  18578  irredn0  20394  drngmul0orOLD  20729  lvecvs0or  21098  lssvs0or  21100  lspsnat  21135  lsppratlem1  21137  domnchr  21522  fctop  22979  cctop  22981  ppttop  22982  clslp  23123  restntr  23157  cnconn  23397  txindis  23609  txconn  23664  isufil2  23883  ufprim  23884  alexsubALTlem3  24024  pmltpc  25427  iundisj2  25526  limcco  25870  fta1b  26147  aalioulem2  26310  abelthlem2  26410  logreclem  26739  dchrfi  27232  2sqb  27409  nosepdmlem  27661  noetasuplem4  27714  lestric  27746  muls0ord  28191  bdayfinbndlem1  28473  tgbtwnconn1  28657  legov3  28680  coltr  28729  colline  28731  tglowdim2ln  28733  ragflat3  28788  ragperp  28799  lmieu  28866  lmicom  28870  lmimid  28876  numedglnl  29227  pthisspthorcycl  29885  nvmul0or  30736  hvmul0or  31111  atomli  32468  atordi  32470  iundisj2f  32675  iundisj2fi  32885  gsumfs2d  33137  mxidlprm  33545  ssmxidl  33549  qsdrng  33572  zarclssn  34033  signsply0  34711  cvmsdisj  35468  nepss  35916  dfon2lem6  35984  btwnconn1lem13  36297  wl-exeq  37873  eqvreldisj  39033  lsator0sp  39461  lkreqN  39630  2at0mat0  39985  trlator0  40631  dochkrshp4  41849  dochsat0  41917  lcfl6  41960  expeqidd  42771  sn-remul0ord  42854  rp-fakeimass  43957  frege124d  44206  clsk1independent  44491  mnringmulrcld  44673  pm10.57  44816  icccncfext  46333  fourierdlem70  46622  ichnreuop  47944  uzlidlring  48723  nneop  49014  mo0sn  49303  euendfunc2  50014