Theorem ord 862

Description: Deduce implication from disjunction. (Contributed by NM, 18-May-1994.)

Hypothesis

Ref	Expression
ord.1	⊢ (𝜑 → (𝜓 ∨ 𝜒))

Assertion

Ref	Expression
ord	⊢ (𝜑 → (¬ 𝜓 → 𝜒))

Proof of Theorem ord

Step	Hyp	Ref	Expression
1		ord.1	. 2 ⊢ (𝜑 → (𝜓 ∨ 𝜒))
2		df-or 846	. 2 ⊢ ((𝜓 ∨ 𝜒) ↔ (¬ 𝜓 → 𝜒))
3	1, 2	sylib 217	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:  olcnd  875  orcanai  1001  ecase2d  1028  oplem1  1055  ornld  1060  ecase23d  1473  19.33b  1888  elpwunsn  4686  disji2  5129  disjxiun  5144  pwssun  5570  swopo  5598  sotric  5615  sotrieq  5616  somo  5624  ordtri3or  6393  ordtri1  6394  suc11  6468  foconst  6817  ordeleqon  7765  ssonprc  7771  onmindif2  7791  limsssuc  7835  limom  7867  onfununi  8337  oeeulem  8597  uniinqs  8787  pw2f1olem  9072  pssnn  9164  pssnnOLD  9261  ordtypelem9  9517  ordtypelem10  9518  oismo  9531  preleqALT  9608  suc11reg  9610  cantnfp1lem2  9670  cantnflem1  9680  cnfcom2lem  9692  cnfcom3lem  9694  rankxpsuc  9873  cardlim  9963  alephdom  10072  cardaleph  10080  iscard3  10084  pwdjudom  10207  cfslbn  10258  fin1a2lem12  10402  gchi  10615  tskssel  10748  inttsk  10765  inar1  10766  r1tskina  10773  tskuni  10774  gruina  10809  grur1  10811  nlt1pi  10897  nqereu  10920  leltne  11299  nneo  12642  zeo2  12645  xrleltne  13120  nltpnft  13139  ngtmnft  13141  xrrebnd  13143  xaddf  13199  xrsupsslem  13282  xrinfmsslem  13283  fzocatel  13692  seqf1olem1  14003  seqf1olem2  14004  znsqcld  14123  discr1  14198  hashnncl  14322  seqcoll2  14422  sqeqd  15109  sqrmo  15194  isercoll  15610  bitsfzo  16372  bitsinv1lem  16378  bitsf1  16383  bezoutlem3  16479  eucalglt  16518  phibndlem  16699  dfphi2  16703  prmdiv  16714  odzdvds  16724  pceq0  16800  pc2dvds  16808  fldivp1  16826  pcfac  16828  prmreclem3  16847  1arith  16856  4sqlem10  16876  4sqlem17  16890  4sqlem18  16891  vdwlem6  16915  ramubcl  16947  ramcl  16958  mrissmrcd  17580  psgnunilem5  19356  oddvdsnn0  19406  odnncl  19407  oddvds  19409  odcl2  19427  gexdvds  19446  gexnnod  19450  sylow1lem1  19460  odcau  19466  pgpssslw  19476  efgs1b  19598  efgredlema  19602  torsubg  19716  prmcyg  19756  gsumval3eu  19766  ablfacrplem  19929  ablfac1eu  19937  ablsimpgprmd  19979  lspdisj  20730  lspsncv0  20751  fidomndrnglem  20917  gzrngunitlem  21002  prmirredlem  21033  fctop  22498  cctop  22500  ppttop  22501  pptbas  22502  ordtrest2lem  22698  connclo  22910  txindis  23129  filconn  23378  ufilb  23401  cldsubg  23606  reconnlem1  24333  reconnlem2  24334  metds0  24357  metdseq0  24361  metnrmlem1a  24365  iccpnfhmeo  24452  xrhmeo  24453  cphsubrglem  24685  minveclem3b  24936  minveclem4a  24938  vitalilem4  25119  itg2gt0  25269  itgsplitioo  25346  limccnp2  25400  rollelem  25497  dvlip  25501  itgsubstlem  25556  plyaddlem1  25718  plymullem1  25719  coefv0  25753  dgreq0  25770  radcnv0  25919  pserdvlem2  25931  pilem2  25955  sineq0  26024  logtayl  26159  cxpsqrt  26202  isosctrlem2  26313  atantayl2  26432  rlimcnp2  26460  amgm  26484  basellem3  26576  muval2  26627  sqf11  26632  ppinprm  26645  chtnprm  26647  perfectlem2  26722  lgsdir  26824  lgsabs1  26828  lgseisenlem1  26867  2sqlem7  26916  2sqblem  26923  2sqmod  26928  2sqreultblem  26940  2sqreunnltblem  26943  chebbnd1lem1  26961  dchrisum0flblem1  27000  pntpbnd1  27078  pntpbnd2  27079  ostth  27131  nosepon  27157  symquadlem  27929  midexlem  27932  colperp  27969  midex  27977  oppperpex  27993  hlpasch  27996  hpgerlem  28005  colopp  28009  lmieu  28024  lmicom  28028  trgcopy  28044  cgracol  28068  minvecolem5  30121  staddi  31486  stadd3i  31488  atsseq  31587  atom1d  31593  atoml2i  31623  disji2f  31795  disjif2  31799  fprodex01  32018  psgnfzto1stlem  32246  lvecdim0  32679  ordtrest2NEWlem  32890  eulerpartlemb  33355  sgn3da  33528  subfacp1lem6  34164  cvmscld  34252  cvmsss2  34253  cvmseu  34255  ordtoplem  35308  ordcmp  35320  poimirlem25  36501  heiborlem6  36672  isfldidl  36924  pridlc2  36928  mpobi123f  37018  mptbi12f  37022  ac6s6  37028  lsatcmp  37861  lsatcmp2  37862  2atm  38386  trlatn0  39031  trlval3  39046  cdleme18c  39152  cdlemg17b  39521  cdlemg17i  39528  cdlemh  39676  dia2dimlem2  39924  dia2dimlem3  39925  dochlkr  40244  dochkrshp  40245  lcfl6  40359  lcfrlem9  40409  hdmap14lem6  40732  hgmapval0  40751  ioin9i8  41019  ctbnfien  41541  pw2f1ocnv  41761  unxpwdom3  41822  dgrsub2  41862  dflim5  42064  rp-fakeanorass  42249  mnuprdlem1  43016  mnuprdlem2  43017  mnurndlem1  43025  disjxp1  43741  fmul01lt1lem1  44286  elprn1  44335  stoweidlem35  44737  stirlinglem5  44780  stirlinglem12  44787  fourierdlem42  44851  fourierdlem93  44901  perfectALTVlem2  46376