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  1882  axi12  2791  r19.30  3338  sspss  4076  eqoreldif  4622  pwpw0  4746  sssn  4759  pwsnOLD  4831  unissint  4900  disjiund  5056  disjxiun  5063  otsndisj  5409  otiunsndisj  5410  pwssun  5456  isso2i  5508  ordtr3  6236  ordtri2or  6286  unizlim  6307  fvclss  7001  orduniorsuc  7545  ordzsl  7560  nn0suc  7606  xpexr  7623  odi  8205  swoso  8322  erdisj  8341  ordtypelem7  8988  wemapsolem  9014  domwdom  9038  iscard3  9519  ackbij1lem18  9659  fin56  9815  entric  9979  gchdomtri  10051  inttsk  10196  r1tskina  10204  psslinpr  10453  ssxr  10710  letric  10740  mul0or  11280  mulge0b  11510  zeo  12069  uzm1  12277  xrletri  12547  supxrgtmnf  12723  sq01  13587  ruclem3  15586  prm2orodd  16035  phiprmpw  16113  pleval2i  17574  irredn0  19453  drngmul0or  19523  lvecvs0or  19880  lssvs0or  19882  lspsnat  19917  lsppratlem1  19919  domnchr  20679  fctop  21612  cctop  21614  ppttop  21615  clslp  21756  restntr  21790  cnconn  22030  txindis  22242  txconn  22297  isufil2  22516  ufprim  22517  alexsubALTlem3  22657  pmltpc  24051  iundisj2  24150  limcco  24491  fta1b  24763  aalioulem2  24922  abelthlem2  25020  logreclem  25340  dchrfi  25831  2sqb  26008  tgbtwnconn1  26361  legov3  26384  coltr  26433  colline  26435  tglowdim2ln  26437  ragflat3  26492  ragperp  26503  lmieu  26570  lmicom  26574  lmimid  26580  numedglnl  26929  nvmul0or  28427  hvmul0or  28802  atomli  30159  atordi  30161  iundisj2f  30340  iundisj2fi  30520  mxidlprm  30977  ssmxidl  30979  signsply0  31821  pthisspthorcycl  32375  cvmsdisj  32517  nepss  32948  dfon2lem6  33033  soseq  33096  nosepdmlem  33187  noetalem3  33219  btwnconn1lem13  33560  wl-exeq  34789  eqvreldisj  35864  lsator0sp  36152  lkreqN  36321  2at0mat0  36676  trlator0  37322  dochkrshp4  38540  dochsat0  38608  lcfl6  38651  rp-fakeimass  39898  frege124d  40126  clsk1independent  40416  pm10.57  40723  icccncfext  42190  fourierdlem70  42481  ichnreuop  43654  uzlidlring  44220  nneop  44606