Theorem ord 865

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 849	. 2 ⊢ ((𝜓 ∨ 𝜒) ↔ (¬ 𝜓 → 𝜒))
3	1, 2	sylib 218	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:  olcnd  878  orcanai  1005  ecase2d  1032  oplem1  1057  ornld  1062  19.33b  1887  elpwunsn  4628  disji2  5069  disjxiun  5082  pwssun  5523  swopo  5550  sotric  5569  sotrieq  5570  somo  5578  ordtri3or  6355  ordtri1  6356  suc11  6432  foconst  6767  ordeleqon  7736  ssonprc  7741  onmindif2  7761  limsssuc  7801  limom  7833  onfununi  8281  oeeulem  8537  uniinqs  8744  pw2f1olem  9019  pssnn  9103  ordtypelem9  9441  ordtypelem10  9442  oismo  9455  preleqALT  9538  suc11reg  9540  cantnfp1lem2  9600  cantnflem1  9610  cnfcom2lem  9622  cnfcom3lem  9624  rankxpsuc  9806  cardlim  9896  alephdom  10003  cardaleph  10011  iscard3  10015  pwdjudom  10137  cfslbn  10189  fin1a2lem12  10333  gchi  10547  tskssel  10680  inttsk  10697  inar1  10698  r1tskina  10705  tskuni  10706  gruina  10741  grur1  10743  nlt1pi  10829  nqereu  10852  leltne  11235  nneo  12613  zeo2  12616  xrleltne  13096  nltpnft  13116  ngtmnft  13118  xrrebnd  13120  xaddf  13176  xrsupsslem  13259  xrinfmsslem  13260  fzocatel  13684  seqf1olem1  14003  seqf1olem2  14004  znsqcld  14124  discr1  14201  hashnncl  14328  seqcoll2  14427  sqeqd  15128  sqrmo  15213  isercoll  15630  bitsfzo  16404  bitsinv1lem  16410  bitsf1  16415  bezoutlem3  16510  eucalglt  16554  phibndlem  16740  dfphi2  16744  prmdiv  16755  odzdvds  16766  pceq0  16842  pc2dvds  16850  fldivp1  16868  pcfac  16870  prmreclem3  16889  1arith  16898  4sqlem10  16918  4sqlem17  16932  4sqlem18  16933  vdwlem6  16957  ramubcl  16989  ramcl  17000  mrissmrcd  17606  psgnunilem5  19469  oddvdsnn0  19519  odnncl  19520  oddvds  19522  odcl2  19540  gexdvds  19559  gexnnod  19563  sylow1lem1  19573  odcau  19579  pgpssslw  19589  efgs1b  19711  efgredlema  19715  torsubg  19829  prmcyg  19869  gsumval3eu  19879  ablfacrplem  20042  ablfac1eu  20050  ablsimpgprmd  20092  fidomndrnglem  20749  lspdisj  21123  lspsncv0  21144  gzrngunitlem  21412  prmirredlem  21452  fctop  22969  cctop  22971  ppttop  22972  pptbas  22973  ordtrest2lem  23168  connclo  23380  txindis  23599  filconn  23848  ufilb  23871  cldsubg  24076  reconnlem1  24792  reconnlem2  24793  metds0  24816  metdseq0  24820  metnrmlem1a  24824  iccpnfhmeo  24912  xrhmeo  24913  cphsubrglem  25144  minveclem3b  25395  minveclem4a  25397  vitalilem4  25578  itg2gt0  25727  itgsplitioo  25805  limccnp2  25859  rollelem  25956  dvlip  25960  itgsubstlem  26015  plyaddlem1  26178  plymullem1  26179  coefv0  26213  dgreq0  26230  radcnv0  26381  pserdvlem2  26393  pilem2  26417  sineq0  26488  logtayl  26624  cxpsqrt  26667  isosctrlem2  26783  atantayl2  26902  rlimcnp2  26930  amgm  26954  basellem3  27046  muval2  27097  sqf11  27102  ppinprm  27115  chtnprm  27117  perfectlem2  27193  lgsdir  27295  lgsabs1  27299  lgseisenlem1  27338  2sqlem7  27387  2sqblem  27394  2sqmod  27399  2sqreultblem  27411  2sqreunnltblem  27414  chebbnd1lem1  27432  dchrisum0flblem1  27471  pntpbnd1  27549  pntpbnd2  27550  ostth  27602  nosepon  27629  abssge0  28237  elnns2  28333  dfnns2  28364  z12bday  28477  symquadlem  28757  midexlem  28760  colperp  28797  midex  28805  oppperpex  28821  hlpasch  28824  hpgerlem  28833  colopp  28837  lmieu  28852  lmicom  28856  trgcopy  28872  cgracol  28896  minvecolem5  30952  staddi  32317  stadd3i  32319  atsseq  32418  atom1d  32424  atoml2i  32454  disji2f  32647  disjif2  32651  fprodex01  32898  sgn3da  32907  psgnfzto1stlem  33161  lvecdim0  33751  ordtrest2NEWlem  34066  eulerpartlemb  34512  subfacp1lem6  35367  cvmscld  35455  cvmsss2  35456  cvmseu  35458  ordtoplem  36617  ordcmp  36629  poimirlem25  37966  heiborlem6  38137  isfldidl  38389  pridlc2  38393  mpobi123f  38483  mptbi12f  38487  ac6s6  38493  lsatcmp  39449  lsatcmp2  39450  2atm  39973  trlatn0  40618  trlval3  40633  cdleme18c  40739  cdlemg17b  41108  cdlemg17i  41115  cdlemh  41263  dia2dimlem2  41511  dia2dimlem3  41512  dochlkr  41831  dochkrshp  41832  lcfl6  41946  lcfrlem9  41996  hdmap14lem6  42319  hgmapval0  42338  ioin9i8  42646  ctbnfien  43246  pw2f1ocnv  43465  unxpwdom3  43523  dgrsub2  43563  dflim5  43757  rp-fakeanorass  43940  mnuprdlem1  44699  mnuprdlem2  44700  mnurndlem1  44708  disjxp1  45500  fmul01lt1lem1  46014  stoweidlem35  46463  stirlinglem5  46506  stirlinglem12  46513  fourierdlem42  46577  fourierdlem93  46627  perfectALTVlem2  48198