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

This theorem is referenced by:  orc  863  olc  864  pm2.68  897  pm4.79  1000  19.30  1885  axi12  2707  r19.30  3265  r19.30OLD  3266  sspss  4030  eqoreldif  4617  pwpw0  4743  sssn  4756  pwsnOLD  4829  unissint  4900  disjiund  5060  disjxiun  5067  otsndisj  5427  otiunsndisj  5428  pwssun  5476  isso2i  5529  ordtr3  6296  ordtri2or  6346  unizlim  6368  fvclss  7097  orduniorsuc  7652  ordzsl  7667  nn0suc  7716  xpexr  7739  odi  8372  swoso  8489  erdisj  8508  ordtypelem7  9213  wemapsolem  9239  domwdom  9263  iscard3  9780  ackbij1lem18  9924  fin56  10080  entric  10244  gchdomtri  10316  inttsk  10461  r1tskina  10469  psslinpr  10718  ssxr  10975  letric  11005  mul0or  11545  mulge0b  11775  zeo  12336  uzm1  12545  xrletri  12816  supxrgtmnf  12992  sq01  13868  ruclem3  15870  prm2orodd  16324  phiprmpw  16405  pleval2i  17969  irredn0  19860  drngmul0or  19927  lvecvs0or  20285  lssvs0or  20287  lspsnat  20322  lsppratlem1  20324  domnchr  20648  fctop  22062  cctop  22064  ppttop  22065  clslp  22207  restntr  22241  cnconn  22481  txindis  22693  txconn  22748  isufil2  22967  ufprim  22968  alexsubALTlem3  23108  pmltpc  24519  iundisj2  24618  limcco  24962  fta1b  25239  aalioulem2  25398  abelthlem2  25496  logreclem  25817  dchrfi  26308  2sqb  26485  tgbtwnconn1  26840  legov3  26863  coltr  26912  colline  26914  tglowdim2ln  26916  ragflat3  26971  ragperp  26982  lmieu  27049  lmicom  27053  lmimid  27059  numedglnl  27417  nvmul0or  28913  hvmul0or  29288  atomli  30645  atordi  30647  iundisj2f  30830  iundisj2fi  31020  mxidlprm  31542  ssmxidl  31544  zarclssn  31725  signsply0  32430  pthisspthorcycl  32990  cvmsdisj  33132  nepss  33564  dfon2lem6  33670  soseq  33730  nosepdmlem  33813  noetasuplem4  33866  btwnconn1lem13  34328  wl-exeq  35620  eqvreldisj  36654  lsator0sp  36942  lkreqN  37111  2at0mat0  37466  trlator0  38112  dochkrshp4  39330  dochsat0  39398  lcfl6  39441  rp-fakeimass  41017  frege124d  41258  clsk1independent  41545  mnringmulrcld  41735  pm10.57  41878  icccncfext  43318  fourierdlem70  43607  ichnreuop  44812  uzlidlring  45375  nneop  45760  mo0sn  46049