Theorem ord 863

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

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

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 847

This theorem is referenced by:  olcnd  876  orcanai  1003  ecase2d  1030  oplem1  1057  ornld  1062  ecase23d  1473  19.33b  1884  elpwunsn  4707  disji2  5150  disjxiun  5163  pwssun  5590  swopo  5619  sotric  5637  sotrieq  5638  somo  5646  ordtri3or  6427  ordtri1  6428  suc11  6502  foconst  6849  ordeleqon  7817  ssonprc  7823  onmindif2  7843  limsssuc  7887  limom  7919  onfununi  8397  oeeulem  8657  uniinqs  8855  pw2f1olem  9142  pssnn  9234  ordtypelem9  9595  ordtypelem10  9596  oismo  9609  preleqALT  9686  suc11reg  9688  cantnfp1lem2  9748  cantnflem1  9758  cnfcom2lem  9770  cnfcom3lem  9772  rankxpsuc  9951  cardlim  10041  alephdom  10150  cardaleph  10158  iscard3  10162  pwdjudom  10284  cfslbn  10336  fin1a2lem12  10480  gchi  10693  tskssel  10826  inttsk  10843  inar1  10844  r1tskina  10851  tskuni  10852  gruina  10887  grur1  10889  nlt1pi  10975  nqereu  10998  leltne  11379  nneo  12727  zeo2  12730  xrleltne  13207  nltpnft  13226  ngtmnft  13228  xrrebnd  13230  xaddf  13286  xrsupsslem  13369  xrinfmsslem  13370  fzocatel  13780  seqf1olem1  14092  seqf1olem2  14093  znsqcld  14212  discr1  14288  hashnncl  14415  seqcoll2  14514  sqeqd  15215  sqrmo  15300  isercoll  15716  bitsfzo  16481  bitsinv1lem  16487  bitsf1  16492  bezoutlem3  16588  eucalglt  16632  phibndlem  16817  dfphi2  16821  prmdiv  16832  odzdvds  16842  pceq0  16918  pc2dvds  16926  fldivp1  16944  pcfac  16946  prmreclem3  16965  1arith  16974  4sqlem10  16994  4sqlem17  17008  4sqlem18  17009  vdwlem6  17033  ramubcl  17065  ramcl  17076  mrissmrcd  17698  psgnunilem5  19536  oddvdsnn0  19586  odnncl  19587  oddvds  19589  odcl2  19607  gexdvds  19626  gexnnod  19630  sylow1lem1  19640  odcau  19646  pgpssslw  19656  efgs1b  19778  efgredlema  19782  torsubg  19896  prmcyg  19936  gsumval3eu  19946  ablfacrplem  20109  ablfac1eu  20117  ablsimpgprmd  20159  fidomndrnglem  20795  lspdisj  21150  lspsncv0  21171  gzrngunitlem  21473  prmirredlem  21506  fctop  23032  cctop  23034  ppttop  23035  pptbas  23036  ordtrest2lem  23232  connclo  23444  txindis  23663  filconn  23912  ufilb  23935  cldsubg  24140  reconnlem1  24867  reconnlem2  24868  metds0  24891  metdseq0  24895  metnrmlem1a  24899  iccpnfhmeo  24995  xrhmeo  24996  cphsubrglem  25230  minveclem3b  25481  minveclem4a  25483  vitalilem4  25665  itg2gt0  25815  itgsplitioo  25893  limccnp2  25947  rollelem  26047  dvlip  26052  itgsubstlem  26109  plyaddlem1  26272  plymullem1  26273  coefv0  26307  dgreq0  26325  radcnv0  26477  pserdvlem2  26490  pilem2  26514  sineq0  26584  logtayl  26720  cxpsqrt  26763  isosctrlem2  26880  atantayl2  26999  rlimcnp2  27027  amgm  27052  basellem3  27144  muval2  27195  sqf11  27200  ppinprm  27213  chtnprm  27215  perfectlem2  27292  lgsdir  27394  lgsabs1  27398  lgseisenlem1  27437  2sqlem7  27486  2sqblem  27493  2sqmod  27498  2sqreultblem  27510  2sqreunnltblem  27513  chebbnd1lem1  27531  dchrisum0flblem1  27570  pntpbnd1  27648  pntpbnd2  27649  ostth  27701  nosepon  27728  abssge0  28287  elnns2  28362  dfnns2  28380  symquadlem  28715  midexlem  28718  colperp  28755  midex  28763  oppperpex  28779  hlpasch  28782  hpgerlem  28791  colopp  28795  lmieu  28810  lmicom  28814  trgcopy  28830  cgracol  28854  minvecolem5  30913  staddi  32278  stadd3i  32280  atsseq  32379  atom1d  32385  atoml2i  32415  disji2f  32599  disjif2  32603  fprodex01  32829  psgnfzto1stlem  33093  lvecdim0  33619  ordtrest2NEWlem  33868  eulerpartlemb  34333  sgn3da  34506  subfacp1lem6  35153  cvmscld  35241  cvmsss2  35242  cvmseu  35244  ordtoplem  36401  ordcmp  36413  poimirlem25  37605  heiborlem6  37776  isfldidl  38028  pridlc2  38032  mpobi123f  38122  mptbi12f  38126  ac6s6  38132  lsatcmp  38959  lsatcmp2  38960  2atm  39484  trlatn0  40129  trlval3  40144  cdleme18c  40250  cdlemg17b  40619  cdlemg17i  40626  cdlemh  40774  dia2dimlem2  41022  dia2dimlem3  41023  dochlkr  41342  dochkrshp  41343  lcfl6  41457  lcfrlem9  41507  hdmap14lem6  41830  hgmapval0  41849  ioin9i8  42201  ctbnfien  42774  pw2f1ocnv  42994  unxpwdom3  43052  dgrsub2  43092  dflim5  43291  rp-fakeanorass  43475  mnuprdlem1  44241  mnuprdlem2  44242  mnurndlem1  44250  disjxp1  44971  fmul01lt1lem1  45505  elprn1  45554  stoweidlem35  45956  stirlinglem5  45999  stirlinglem12  46006  fourierdlem42  46070  fourierdlem93  46120  perfectALTVlem2  47596