Theorem ord 877

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

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

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 861

This theorem is used by:  olcnd  890  orcanai  1018  ecase2d  1047  oplem1  1072  ornld  1077  19.33b  1915  elpwunsn  4650  disji2  5093  disjxiun  5106  pwssun  5553  swopo  5580  sotric  5599  sotrieq  5600  somo  5608  ordtri3or  6393  ordtri1  6394  suc11  6470  foconst  6807  ordeleqon  7777  ssonprc  7782  onmindif2  7802  limsssuc  7842  limom  7874  onfununi  8324  oeeulem  8583  uniinqs  8791  pw2f1olem  9065  pssnn  9149  ordtypelem9  9484  ordtypelem10  9485  oismo  9498  preleqALT  9582  suc11reg  9584  cantnfp1lem2  9644  cantnflem1  9654  cnfcom2lem  9666  cnfcom3lem  9668  rankxpsuc  9850  cardlim  9963  alephdom  10070  cardaleph  10078  iscard3  10082  pwdjudom  10203  cfslbn  10255  fin1a2lem12  10399  gchi  10613  tskssel  10746  inttsk  10763  inar1  10764  r1tskina  10771  tskuni  10772  gruina  10807  grur1  10809  nlt1pi  10895  nqereu  10918  leltne  11303  nneo  12684  zeo2  12687  xrleltne  13174  nltpnft  13194  ngtmnft  13196  xrrebnd  13198  xaddf  13254  xrsupsslem  13337  xrinfmsslem  13338  fzocatel  13763  seqf1olem1  14082  seqf1olem2  14083  znsqcld  14203  discr1  14280  hashnncl  14407  seqcoll2  14507  sgn3da  15143  sqeqd  15222  sqrmo  15307  isercoll  15724  bitsfzo  16497  bitsinv1lem  16503  bitsf1  16508  bezoutlem3  16603  eucalglt  16647  phibndlem  16833  dfphi2  16837  prmdiv  16848  odzdvds  16859  pceq0  16935  pc2dvds  16943  fldivp1  16961  pcfac  16963  prmreclem3  16982  1arith  16991  4sqlem10  17011  4sqlem17  17025  4sqlem18  17026  vdwlem6  17050  ramubcl  17082  ramcl  17093  mrissmrcd  17700  psgnunilem5  19568  oddvdsnn0  19618  odnncl  19619  oddvds  19621  odcl2  19639  gexdvds  19658  gexnnod  19662  sylow1lem1  19672  odcau  19678  pgpssslw  19688  efgs1b  19810  efgredlema  19814  torsubg  19928  prmcyg  19968  gsumval3eu  19978  ablfacrplem  20141  ablfac1eu  20149  ablsimpgprmd  20191  fidomndrnglem  20885  lspdisj  21258  lspsncv0  21279  prmidlc2  21483  gzrngunitlem  21591  prmirredlem  21631  fctop  23170  cctop  23172  ppttop  23173  pptbas  23174  ordtrest2lem  23369  connclo  23581  txindis  23800  filconn  24049  ufilb  24072  cldsubg  24277  reconnlem1  24993  reconnlem2  24994  metds0  25017  metdseq0  25021  metnrmlem1a  25025  iccpnfhmeo  25113  xrhmeo  25114  cphsubrglem  25345  minveclem3b  25596  minveclem4a  25598  vitalilem4  25779  itg2gt0  25928  itgsplitioo  26006  limccnp2  26060  rollelem  26157  dvlip  26161  itgsubstlem  26216  plyaddlem1  26379  plymullem1  26380  coefv0  26414  dgreq0  26431  radcnv0  26588  pserdvlem2  26600  pilem2  26624  sineq0  26698  logtayl  26834  cxpsqrt  26877  isosctrlem2  26993  atantayl2  27112  rlimcnp2  27140  amgm  27164  basellem3  27256  muval2  27307  sqf11  27312  ppinprm  27325  chtnprm  27327  perfectlem2  27403  lgsdir  27505  lgsabs1  27509  lgseisenlem1  27548  2sqlem7  27597  2sqblem  27604  2sqmod  27609  2sqreultblem  27621  2sqreunnltblem  27624  chebbnd1lem1  27642  dchrisum0flblem1  27681  pntpbnd1  27759  pntpbnd2  27760  ostth  27812  nosepon  27838  abssge0  28447  elnns2  28543  dfnns2  28574  z12bday  28687  symquadlem  28975  midexlem  28978  colperp  29019  midex  29027  oppperpex  29043  hlpasch  29047  hpgerlem  29056  colopp  29060  plngrotlem1  29078  lmieu  29102  lmicom  29106  trgcopy  29124  cgracol  29148  minvecolem5  31242  staddi  32607  stadd3i  32609  atsseq  32708  atom1d  32714  atoml2i  32744  disji2f  32931  disjif2  32935  fprodex01  33178  psgnfzto1stlem  33429  lvecdim0  34006  ordtrest2NEWlem  34321  eulerpartlemb  34767  subfacp1lem6  35685  cvmscld  35773  cvmsss2  35774  cvmseu  35776  ordtoplem  36974  ordcmp  36986  poimirlem25  38324  heiborlem6  38495  isfldidl  38747  pridlc2  38751  mpobi123f  38839  mptbi12f  38843  ac6s6  38849  lsatcmp  39805  lsatcmp2  39806  2atm  40329  trlatn0  40974  trlval3  40989  cdleme18c  41095  cdlemg17b  41464  cdlemg17i  41471  cdlemh  41619  dia2dimlem2  41867  dia2dimlem3  41868  dochlkr  42187  dochkrshp  42188  lcfl6  42302  lcfrlem9  42352  hdmap14lem6  42675  hgmapval0  42694  ioin9i8  43004  ctbnfien  43573  pw2f1ocnv  43792  unxpwdom3  43850  dgrsub2  43890  dflim5  44084  rp-fakeanorass  44267  mnuprdlem1  45010  mnuprdlem2  45011  mnurndlem1  45019  disjxp1  45817  fmul01lt1lem1  46328  stoweidlem35  46777  stirlinglem5  46820  stirlinglem12  46827  fourierdlem42  46891  fourierdlem93  46941  perfectALTVlem2  48515