Theorem orrd 861

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

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

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 206  df-or 846

This theorem is referenced by:  orc  865  olc  866  pm2.68  899  pm4.79  1002  19.30  1884  axi12  2701  r19.30  3120  r19.30OLD  3121  sspss  4099  eqoreldif  4688  pwpw0  4816  sssn  4829  pwsnOLD  4901  unissint  4976  disjiund  5138  disjxiun  5145  otsndisj  5519  otiunsndisj  5520  pwssun  5571  isso2i  5623  ordtr3  6409  ordtri2or  6462  unizlim  6487  fvclss  7240  orduniorsuc  7817  ordzsl  7833  nn0suc  7885  xpexr  7908  soseq  8144  odi  8578  swoso  8735  erdisj  8754  ordtypelem7  9518  wemapsolem  9544  domwdom  9568  iscard3  10087  ackbij1lem18  10231  fin56  10387  entric  10551  gchdomtri  10623  inttsk  10768  r1tskina  10776  psslinpr  11025  ssxr  11282  letric  11313  mul0or  11853  mulge0b  12083  zeo  12647  uzm1  12859  xrletri  13131  supxrgtmnf  13307  sq01  14187  ruclem3  16175  prm2orodd  16627  phiprmpw  16708  pleval2i  18288  irredn0  20236  drngmul0or  20385  lvecvs0or  20720  lssvs0or  20722  lspsnat  20757  lsppratlem1  20759  domnchr  21083  fctop  22506  cctop  22508  ppttop  22509  clslp  22651  restntr  22685  cnconn  22925  txindis  23137  txconn  23192  isufil2  23411  ufprim  23412  alexsubALTlem3  23552  pmltpc  24966  iundisj2  25065  limcco  25409  fta1b  25686  aalioulem2  25845  abelthlem2  25943  logreclem  26264  dchrfi  26755  2sqb  26932  nosepdmlem  27183  noetasuplem4  27236  sletric  27264  tgbtwnconn1  27823  legov3  27846  coltr  27895  colline  27897  tglowdim2ln  27899  ragflat3  27954  ragperp  27965  lmieu  28032  lmicom  28036  lmimid  28042  numedglnl  28401  nvmul0or  29898  hvmul0or  30273  atomli  31630  atordi  31632  iundisj2f  31816  iundisj2fi  32003  mxidlprm  32581  ssmxidl  32585  qsdrng  32606  zarclssn  32848  signsply0  33557  pthisspthorcycl  34114  cvmsdisj  34256  nepss  34682  dfon2lem6  34755  btwnconn1lem13  35066  wl-exeq  36398  eqvreldisj  37479  lsator0sp  37866  lkreqN  38035  2at0mat0  38391  trlator0  39037  dochkrshp4  40255  dochsat0  40323  lcfl6  40366  rp-fakeimass  42253  frege124d  42502  clsk1independent  42787  mnringmulrcld  42977  pm10.57  43120  icccncfext  44593  fourierdlem70  44882  ichnreuop  46130  uzlidlring  46817  nneop  47202  mo0sn  47490