Theorem orrd 859

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

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

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 209  df-or 844

This theorem is referenced by:  orc  863  olc  864  pm2.68  897  pm4.79  1000  19.30  1878  axi12  2789  axi12OLD  2790  axbndOLD  2792  r19.30  3338  sspss  4075  eqoreldif  4615  pwpw0  4739  sssn  4752  pwsnALT  4824  unissint  4892  disjiund  5048  disjxiun  5055  otsndisj  5401  otiunsndisj  5402  pwssun  5449  isso2i  5502  ordtr3  6230  ordtri2or  6280  unizlim  6301  fvclss  6995  orduniorsuc  7539  ordzsl  7554  nn0suc  7600  xpexr  7617  odi  8199  swoso  8316  erdisj  8335  ordtypelem7  8982  wemapsolem  9008  domwdom  9032  iscard3  9513  ackbij1lem18  9653  fin56  9809  entric  9973  gchdomtri  10045  inttsk  10190  r1tskina  10198  psslinpr  10447  ssxr  10704  letric  10734  mul0or  11274  mulge0b  11504  zeo  12062  uzm1  12270  xrletri  12540  supxrgtmnf  12716  sq01  13580  ruclem3  15580  prm2orodd  16029  phiprmpw  16107  pleval2i  17568  irredn0  19447  drngmul0or  19517  lvecvs0or  19874  lssvs0or  19876  lspsnat  19911  lsppratlem1  19913  domnchr  20673  fctop  21606  cctop  21608  ppttop  21609  clslp  21750  restntr  21784  cnconn  22024  txindis  22236  txconn  22291  isufil2  22510  ufprim  22511  alexsubALTlem3  22651  pmltpc  24045  iundisj2  24144  limcco  24485  fta1b  24757  aalioulem2  24916  abelthlem2  25014  logreclem  25334  dchrfi  25825  2sqb  26002  tgbtwnconn1  26355  legov3  26378  coltr  26427  colline  26429  tglowdim2ln  26431  ragflat3  26486  ragperp  26497  lmieu  26564  lmicom  26568  lmimid  26574  numedglnl  26923  nvmul0or  28421  hvmul0or  28796  atomli  30153  atordi  30155  iundisj2f  30334  iundisj2fi  30514  mxidlprm  30972  ssmxidl  30974  signsply0  31816  pthisspthorcycl  32370  cvmsdisj  32512  nepss  32943  dfon2lem6  33028  soseq  33091  nosepdmlem  33182  noetalem3  33214  btwnconn1lem13  33555  wl-exeq  34768  eqvreldisj  35843  lsator0sp  36131  lkreqN  36300  2at0mat0  36655  trlator0  37301  dochkrshp4  38519  dochsat0  38587  lcfl6  38630  rp-fakeimass  39871  frege124d  40099  clsk1independent  40389  pm10.57  40696  icccncfext  42163  fourierdlem70  42455  ichnreuop  43628  uzlidlring  44194  nneop  44580