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  7243  orduniorsuc  7820  ordzsl  7836  nn0suc  7888  xpexr  7911  soseq  8147  odi  8581  swoso  8738  erdisj  8757  ordtypelem7  9521  wemapsolem  9547  domwdom  9571  iscard3  10090  ackbij1lem18  10234  fin56  10390  entric  10554  gchdomtri  10626  inttsk  10771  r1tskina  10779  psslinpr  11028  ssxr  11285  letric  11316  mul0or  11856  mulge0b  12086  zeo  12650  uzm1  12862  xrletri  13134  supxrgtmnf  13310  sq01  14190  ruclem3  16178  prm2orodd  16630  phiprmpw  16711  pleval2i  18291  irredn0  20241  drngmul0or  20390  lvecvs0or  20727  lssvs0or  20729  lspsnat  20764  lsppratlem1  20766  domnchr  21090  fctop  22514  cctop  22516  ppttop  22517  clslp  22659  restntr  22693  cnconn  22933  txindis  23145  txconn  23200  isufil2  23419  ufprim  23420  alexsubALTlem3  23560  pmltpc  24974  iundisj2  25073  limcco  25417  fta1b  25694  aalioulem2  25853  abelthlem2  25951  logreclem  26274  dchrfi  26765  2sqb  26942  nosepdmlem  27193  noetasuplem4  27246  sletric  27274  tgbtwnconn1  27864  legov3  27887  coltr  27936  colline  27938  tglowdim2ln  27940  ragflat3  27995  ragperp  28006  lmieu  28073  lmicom  28077  lmimid  28083  numedglnl  28442  nvmul0or  29941  hvmul0or  30316  atomli  31673  atordi  31675  iundisj2f  31859  iundisj2fi  32046  mxidlprm  32631  ssmxidl  32635  qsdrng  32656  zarclssn  32922  signsply0  33631  pthisspthorcycl  34188  cvmsdisj  34330  nepss  34762  dfon2lem6  34835  btwnconn1lem13  35146  wl-exeq  36495  eqvreldisj  37576  lsator0sp  37963  lkreqN  38132  2at0mat0  38488  trlator0  39134  dochkrshp4  40352  dochsat0  40420  lcfl6  40463  rp-fakeimass  42351  frege124d  42600  clsk1independent  42885  mnringmulrcld  43075  pm10.57  43218  icccncfext  44688  fourierdlem70  44977  ichnreuop  46225  uzlidlring  46912  nneop  47296  mo0sn  47584