Theorem orrd 864

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

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

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 207  df-or 849

This theorem is referenced by:  orc  868  olc  869  pm2.68  901  pm4.79  1006  19.30  1883  axi12  2706  r19.30  3104  sspss  4042  eqoreldif  4629  pwpw0  4756  sssn  4769  unissint  4914  disjiund  5076  disjxiun  5082  otsndisj  5473  otiunsndisj  5474  pwssun  5523  isso2i  5576  ordtr3  6369  ordtri2or  6423  unizlim  6447  fvclss  7196  orduniorsuc  7781  ordzsl  7796  nn0suc  7845  xpexr  7869  soseq  8109  odi  8514  swoso  8678  erdisj  8701  ordtypelem7  9439  wemapsolem  9465  domwdom  9489  iscard3  10015  ackbij1lem18  10158  fin56  10315  entric  10479  gchdomtri  10552  inttsk  10697  r1tskina  10705  psslinpr  10954  1re  11144  ssxr  11215  letric  11246  mul0or  11790  mulge0b  12026  zeo  12615  uzm1  12822  xrletri  13104  supxrgtmnf  13281  sq01  14187  ruclem3  16200  prm2orodd  16660  phiprmpw  16746  pleval2i  18300  chnind  18587  irredn0  20403  drngmul0orOLD  20738  lvecvs0or  21106  lssvs0or  21108  lspsnat  21143  lsppratlem1  21145  domnchr  21512  fctop  22969  cctop  22971  ppttop  22972  clslp  23113  restntr  23147  cnconn  23387  txindis  23599  txconn  23654  isufil2  23873  ufprim  23874  alexsubALTlem3  24014  pmltpc  25417  iundisj2  25516  limcco  25860  fta1b  26137  aalioulem2  26299  abelthlem2  26397  logreclem  26726  dchrfi  27218  2sqb  27395  nosepdmlem  27647  noetasuplem4  27700  lestric  27732  muls0ord  28177  bdayfinbndlem1  28459  tgbtwnconn1  28643  legov3  28666  coltr  28715  colline  28717  tglowdim2ln  28719  ragflat3  28774  ragperp  28785  lmieu  28852  lmicom  28856  lmimid  28862  numedglnl  29213  pthisspthorcycl  29870  nvmul0or  30721  hvmul0or  31096  atomli  32453  atordi  32455  iundisj2f  32660  iundisj2fi  32870  gsumfs2d  33122  mxidlprm  33530  ssmxidl  33534  qsdrng  33557  zarclssn  34017  signsply0  34695  cvmsdisj  35452  nepss  35900  dfon2lem6  35968  btwnconn1lem13  36281  wl-exeq  37859  eqvreldisj  39019  lsator0sp  39447  lkreqN  39616  2at0mat0  39971  trlator0  40617  dochkrshp4  41835  dochsat0  41903  lcfl6  41946  expeqidd  42757  sn-remul0ord  42840  rp-fakeimass  43939  frege124d  44188  clsk1independent  44473  mnringmulrcld  44655  pm10.57  44798  icccncfext  46315  fourierdlem70  46604  ichnreuop  47932  uzlidlring  48711  nneop  49002  mo0sn  49291  euendfunc2  50002