Theorem ord 870

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 854	. 2 ⊢ ((𝜓 ∨ 𝜒) ↔ (¬ 𝜓 → 𝜒))
3	1, 2	sylib 219	1 ⊢ (𝜑 → (¬ 𝜓 → 𝜒))

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

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 208  df-or 854

This theorem is referenced by:  olcnd  883  orcanai  1010  ecase2d  1037  oplem1  1062  ornld  1067  19.33b  1892  elpwunsn  4616  disji2  5056  disjxiun  5069  pwssun  5510  swopo  5537  sotric  5556  sotrieq  5557  somo  5565  ordtri3or  6342  ordtri1  6343  suc11  6419  foconst  6754  ordeleqon  7725  ssonprc  7730  onmindif2  7750  limsssuc  7790  limom  7822  onfununi  8271  oeeulem  8527  uniinqs  8734  pw2f1olem  9009  pssnn  9093  ordtypelem9  9431  ordtypelem10  9432  oismo  9445  preleqALT  9529  suc11reg  9531  cantnfp1lem2  9591  cantnflem1  9601  cnfcom2lem  9613  cnfcom3lem  9615  rankxpsuc  9797  cardlim  9887  alephdom  9994  cardaleph  10002  iscard3  10006  pwdjudom  10128  cfslbn  10180  fin1a2lem12  10324  gchi  10538  tskssel  10671  inttsk  10688  inar1  10689  r1tskina  10696  tskuni  10697  gruina  10732  grur1  10734  nlt1pi  10820  nqereu  10843  leltne  11226  nneo  12604  zeo2  12607  xrleltne  13087  nltpnft  13107  ngtmnft  13109  xrrebnd  13111  xaddf  13167  xrsupsslem  13250  xrinfmsslem  13251  fzocatel  13675  seqf1olem1  13994  seqf1olem2  13995  znsqcld  14115  discr1  14192  hashnncl  14319  seqcoll2  14418  sqeqd  15119  sqrmo  15204  isercoll  15621  bitsfzo  16395  bitsinv1lem  16401  bitsf1  16406  bezoutlem3  16501  eucalglt  16545  phibndlem  16731  dfphi2  16735  prmdiv  16746  odzdvds  16757  pceq0  16833  pc2dvds  16841  fldivp1  16859  pcfac  16861  prmreclem3  16880  1arith  16889  4sqlem10  16909  4sqlem17  16923  4sqlem18  16924  vdwlem6  16948  ramubcl  16980  ramcl  16991  mrissmrcd  17597  psgnunilem5  19460  oddvdsnn0  19510  odnncl  19511  oddvds  19513  odcl2  19531  gexdvds  19550  gexnnod  19554  sylow1lem1  19564  odcau  19570  pgpssslw  19580  efgs1b  19702  efgredlema  19706  torsubg  19820  prmcyg  19860  gsumval3eu  19870  ablfacrplem  20033  ablfac1eu  20041  ablsimpgprmd  20083  fidomndrnglem  20744  lspdisj  21118  lspsncv0  21139  gzrngunitlem  21407  prmirredlem  21447  fctop  22987  cctop  22989  ppttop  22990  pptbas  22991  ordtrest2lem  23186  connclo  23398  txindis  23617  filconn  23866  ufilb  23889  cldsubg  24094  reconnlem1  24810  reconnlem2  24811  metds0  24834  metdseq0  24838  metnrmlem1a  24842  iccpnfhmeo  24930  xrhmeo  24931  cphsubrglem  25162  minveclem3b  25413  minveclem4a  25415  vitalilem4  25596  itg2gt0  25745  itgsplitioo  25823  limccnp2  25877  rollelem  25974  dvlip  25978  itgsubstlem  26033  plyaddlem1  26196  plymullem1  26197  coefv0  26231  dgreq0  26248  radcnv0  26399  pserdvlem2  26411  pilem2  26435  sineq0  26506  logtayl  26642  cxpsqrt  26685  isosctrlem2  26801  atantayl2  26920  rlimcnp2  26948  amgm  26972  basellem3  27064  muval2  27115  sqf11  27120  ppinprm  27133  chtnprm  27135  perfectlem2  27211  lgsdir  27313  lgsabs1  27317  lgseisenlem1  27356  2sqlem7  27405  2sqblem  27412  2sqmod  27417  2sqreultblem  27429  2sqreunnltblem  27432  chebbnd1lem1  27450  dchrisum0flblem1  27489  pntpbnd1  27567  pntpbnd2  27568  ostth  27620  nosepon  27647  abssge0  28255  elnns2  28351  dfnns2  28382  z12bday  28495  symquadlem  28775  midexlem  28778  colperp  28815  midex  28823  oppperpex  28839  hlpasch  28842  hpgerlem  28851  colopp  28855  lmieu  28870  lmicom  28874  trgcopy  28890  cgracol  28914  minvecolem5  30970  staddi  32335  stadd3i  32337  atsseq  32436  atom1d  32442  atoml2i  32472  disji2f  32666  disjif2  32670  fprodex01  32917  sgn3da  32926  psgnfzto1stlem  33181  lvecdim0  33791  ordtrest2NEWlem  34106  eulerpartlemb  34552  subfacp1lem6  35413  cvmscld  35501  cvmsss2  35502  cvmseu  35504  ordtoplem  36663  ordcmp  36675  poimirlem25  38012  heiborlem6  38183  isfldidl  38435  pridlc2  38439  mpobi123f  38529  mptbi12f  38533  ac6s6  38539  lsatcmp  39495  lsatcmp2  39496  2atm  40019  trlatn0  40664  trlval3  40679  cdleme18c  40785  cdlemg17b  41154  cdlemg17i  41161  cdlemh  41309  dia2dimlem2  41557  dia2dimlem3  41558  dochlkr  41877  dochkrshp  41878  lcfl6  41992  lcfrlem9  42042  hdmap14lem6  42365  hgmapval0  42384  ioin9i8  42692  ctbnfien  43263  pw2f1ocnv  43482  unxpwdom3  43540  dgrsub2  43580  dflim5  43774  rp-fakeanorass  43957  mnuprdlem1  44716  mnuprdlem2  44717  mnurndlem1  44725  disjxp1  45517  fmul01lt1lem1  46029  stoweidlem35  46478  stirlinglem5  46521  stirlinglem12  46528  fourierdlem42  46592  fourierdlem93  46642  perfectALTVlem2  48213