Theorem orrd 876

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

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

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 210  df-or 861

This theorem is referenced by:  orc  880  olc  881  pm2.68  913  pm4.79  1019  19.30  1904  axi12  2735  r19.30  3132  sspss  4058  eqoreldif  4647  pwpw0  4774  sssn  4787  unissint  4932  disjiund  5095  disjxiun  5101  otsndisj  5492  otiunsndisj  5493  pwssun  5543  isso2i  5596  ordtr3  6396  ordtri2or  6450  unizlim  6474  fvclss  7229  orduniorsuc  7814  ordzsl  7829  nn0suc  7879  xpexr  7903  soseq  8143  odi  8552  swoso  8717  erdisj  8740  ordtypelem7  9474  wemapsolem  9500  domwdom  9524  iscard3  10065  ackbij1lem18  10207  fin56  10365  entric  10529  gchdomtri  10602  inttsk  10747  r1tskina  10755  psslinpr  11004  1re  11196  ssxr  11267  letric  11298  mul0or  11842  mulge0b  12073  zeo  12670  uzm1  12884  xrletri  13166  supxrgtmnf  13343  sq01  14249  ruclem3  16277  prm2orodd  16737  phiprmpw  16823  pleval2i  18378  chnind  18665  irredn0  20493  lvecvs0or  21198  lssvs0or  21200  lspsnat  21235  lsppratlem1  21237  domnchr  21639  fctop  23118  cctop  23120  ppttop  23121  clslp  23262  restntr  23296  cnconn  23536  txindis  23748  txconn  23803  isufil2  24022  ufprim  24023  alexsubALTlem3  24163  pmltpc  25566  iundisj2  25665  limcco  26009  fta1b  26286  aalioulem2  26451  abelthlem2  26549  logreclem  26881  dchrfi  27373  2sqb  27550  nosepdmlem  27801  noetasuplem4  27854  lestric  27886  muls0ord  28332  bdayfinbndlem1  28614  tgbtwnconn1  28798  legov3  28821  coltr  28871  colline  28873  tglowdim2ln  28875  ragflat3  28933  ragperp  28944  lmieu  29032  lmicom  29036  lmimid  29042  numedglnl  29399  pthisspthorcycl  30056  nvmul0or  30907  hvmul0or  31282  atomli  32639  atordi  32641  iundisj2f  32841  iundisj2fi  33050  gsumfs2d  33289  mxidlprm  33665  ssmxidl  33669  qsdrng  33691  dflringlem3  33698  dflring4  33700  zarclssn  34175  signsply0  34850  cvmsdisj  35628  nepss  36076  dfon2lem6  36144  btwnconn1lem13  36457  wl-exeq  38044  eqvreldisj  39204  lsator0sp  39632  lkreqN  39801  2at0mat0  40156  trlator0  40802  dochkrshp4  42020  dochsat0  42088  lcfl6  42131  expeqidd  42941  sn-remul0ord  43024  rp-fakeimass  44095  frege124d  44344  clsk1independent  44629  mnringmulrcld  44811  pm10.57  44940  icccncfext  46460  fourierdlem70  46749  ichnreuop  48077  uzlidlring  48856  nneop  49158  mo0sn  49446  euendfunc2  50157