Theorem orrd 877

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  orc  881  olc  882  pm2.68  914  pm4.79  1021  19.30  1914  axi12  2736  r19.30  3135  sspss  4059  eqoreldif  4656  pwpw0  4784  sssn  4797  unissint  4942  disjiund  5105  disjxiun  5111  otsndisj  5507  otiunsndisj  5508  pwssun  5558  isso2i  5611  ordtr3  6414  ordtri2or  6468  unizlim  6492  fvclss  7246  orduniorsuc  7835  ordzsl  7850  nn0suc  7900  xpexr  7924  soseq  8164  odi  8573  swoso  8738  erdisj  8761  ordtypelem7  9496  wemapsolem  9522  domwdom  9546  iscard3  10096  ackbij1lem18  10238  fin56  10395  entric  10559  gchdomtri  10632  inttsk  10777  r1tskina  10785  psslinpr  11034  1re  11226  ssxr  11297  letric  11328  mul0or  11872  mulge0b  12103  zeo  12700  uzm1  12914  xrletri  13196  supxrgtmnf  13373  sq01  14281  ruclem3  16314  prm2orodd  16774  phiprmpw  16860  pleval2i  18415  chnind  18702  irredn0  20538  lvecvs0or  21269  lssvs0or  21271  lspsnat  21306  lsppratlem1  21308  domnchr  21719  fctop  23198  cctop  23200  ppttop  23201  clslp  23342  restntr  23376  cnconn  23616  txindis  23828  txconn  23883  isufil2  24102  ufprim  24103  alexsubALTlem3  24243  pmltpc  25646  iundisj2  25745  limcco  26089  fta1b  26366  aalioulem2  26533  abelthlem2  26632  logreclem  26964  dchrfi  27456  2sqb  27633  nosepdmlem  27884  noetasuplem4  27937  lestric  27969  muls0ord  28415  bdayfinbndlem1  28697  tgbtwnconn1  28881  legov3  28904  coltr  28958  colline  28960  tglowdim2ln  28962  ragflat3  29023  ragperp  29034  lmieu  29130  lmicom  29134  lmimid  29140  numedglnl  29531  pthisspthorcycl  30188  nvmul0or  31039  hvmul0or  31414  atomli  32771  atordi  32773  iundisj2f  32972  iundisj2fi  33179  gsumfs2d  33412  mxidlprm  33784  ssmxidl  33788  qsdrng  33810  dflringlem3  33817  dflring4  33819  zarclssn  34294  signsply0  34970  cvmsdisj  35783  nepss  36231  dfon2lem6  36299  btwnconn1lem13  36612  wl-exeq  38230  eqvreldisj  39388  lsator0sp  39816  lkreqN  39985  2at0mat0  40340  trlator0  40986  dochkrshp4  42204  dochsat0  42272  lcfl6  42315  expeqidd  43127  sn-remul0ord  43210  rp-fakeimass  44279  frege124d  44528  clsk1independent  44813  mnringmulrcld  44993  pm10.57  45122  icccncfext  46642  fourierdlem70  46931  ichnreuop  48262  uzlidlring  49041  nneop  49347  mo0sn  49635  euendfunc2  50346