Theorem ord 878

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

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

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 862

This theorem is used by:  olcnd  891  orcanai  1018  ecase2d  1047  oplem1  1072  ornld  1077  19.33b  1919  elpwunsn  4645  disji2  5090  disjxiun  5103  pwssun  5547  swopo  5574  sotric  5593  sotrieq  5594  somo  5602  ordtri3or  6402  ordtri1  6403  suc11  6479  foconst  6822  ordeleqon  7806  ssonprc  7811  onmindif2  7831  limsssuc  7871  limom  7903  onfununi  8363  oeeulem  8624  uniinqs  8832  pw2f1olem  9114  pssnn  9198  ordtypelem9  9533  ordtypelem10  9534  oismo  9547  preleqALT  9631  suc11reg  9633  cantnfp1lem2  9693  cantnflem1  9703  cnfcom2lem  9715  cnfcom3lem  9717  rankxpsuc  9912  cardlim  10066  alephdom  10173  cardaleph  10181  iscard3  10185  pwdjudom  10306  cfslbn  10358  fin1a2lem12  10502  gchi  10722  tskssel  10855  inttsk  10872  inar1  10873  r1tskina  10880  tskuni  10881  gruina  10916  grur1  10918  nlt1pi  11004  nqereu  11027  leltne  11412  nneo  12796  zeo2  12799  xrleltne  13287  nltpnft  13307  ngtmnft  13309  xrrebnd  13311  xaddf  13367  xrsupsslem  13450  xrinfmsslem  13451  fzocatel  13877  seqf1olem1  14197  seqf1olem2  14198  znsqcld  14318  discr1  14396  hashnncl  14523  seqcoll2  14623  sgn3da  15269  sqeqd  15348  sqrmo  15433  isercoll  15850  bitsfzo  16620  bitsinv1lem  16626  bitsf1  16631  bezoutlem3  16729  eucalglt  16775  phibndlem  16962  dfphi2  16966  prmdiv  16977  odzdvds  16988  pceq0  17064  pc2dvds  17072  fldivp1  17090  pcfac  17092  prmreclem3  17111  1arith  17120  4sqlem10  17140  4sqlem17  17154  4sqlem18  17155  vdwlem6  17179  ramubcl  17211  ramcl  17222  mrissmrcd  17829  psgnunilem5  19723  oddvdsnn0  19773  odnncl  19774  oddvds  19776  odcl2  19794  gexdvds  19813  gexnnod  19817  sylow1lem1  19827  odcau  19833  pgpssslw  19843  efgs1b  19965  efgredlema  19969  torsubg  20083  prmcyg  20123  gsumval3eu  20133  ablfacrplem  20296  ablfac1eu  20304  ablsimpgprmd  20346  fidomndrnglem  21045  lspdisj  21418  lspsncv0  21439  prmidlc2  21645  gzrngunitlem  21753  prmirredlem  21793  fctop  23337  cctop  23339  ppttop  23340  pptbas  23341  ordtrest2lem  23536  connclo  23748  txindis  23968  filconn  24217  ufilb  24240  cldsubg  24445  reconnlem1  25161  reconnlem2  25162  metds0  25185  metdseq0  25189  metnrmlem1a  25193  iccpnfhmeo  25281  xrhmeo  25282  cphsubrglem  25513  minveclem3b  25764  minveclem4a  25766  vitalilem4  25947  itg2gt0  26096  itgsplitioo  26173  limccnp2  26227  rollelem  26324  dvlip  26328  itgsubstlem  26383  plyaddlem1  26547  plymullem1  26548  coefv0  26582  dgreq0  26599  radcnv0  26758  pserdvlem2  26770  pilem2  26794  sineq0  26867  logtayl  27003  cxpsqrt  27046  isosctrlem2  27162  atantayl2  27281  rlimcnp2  27309  amgm  27333  basellem3  27425  muval2  27476  sqf11  27481  chtnprm  27496  perfectlem2  27572  lgsdir  27674  lgsabs1  27678  lgseisenlem1  27717  2sqlem7  27766  2sqblem  27773  2sqmod  27778  2sqreultblem  27790  2sqreunnltblem  27793  chebbnd1lem1  27811  dchrisum0flblem1  27850  pntpbnd1  27928  pntpbnd2  27929  ostth  27981  nosepon  28037  abssge0  28646  elnns2  28742  dfnns2  28773  z12bday  28886  symquadlem  29176  midexlem  29179  colperp  29220  midex  29228  oppperpex  29244  hlpasch  29249  hpgerlem  29258  colopp  29262  plngrotlem1  29280  lmieu  29304  lmicom  29308  trgcopy  29326  cgracol  29351  minvecolem5  31498  staddi  32863  stadd3i  32865  atsseq  32964  atom1d  32970  atoml2i  33000  disji2f  33228  disjif2  33232  fprodex01  33472  psgnfzto1stlem  33717  lvecdim0  34295  ordtrest2NEWlem  34610  eulerpartlemb  35056  ordunmax  35775  subfacp1lem6  36074  cvmscld  36162  cvmsss2  36163  cvmseu  36165  ordtoplem  37353  ordcmp  37365  poimirlem25  38706  heiborlem6  38893  isfldidl  39145  pridlc2  39149  mpobi123f  39237  mptbi12f  39241  ac6s6  39247  lsatcmp  40203  lsatcmp2  40204  2atm  40727  trlatn0  41372  trlval3  41387  cdleme18c  41493  cdlemg17b  41862  cdlemg17i  41869  cdlemh  42017  dia2dimlem2  42265  dia2dimlem3  42266  dochlkr  42585  dochkrshp  42586  lcfl6  42700  lcfrlem9  42750  hdmap14lem6  43073  hgmapval0  43092  ioin9i8  43402  ctbnfien  43968  pw2f1ocnv  44187  unxpwdom3  44240  dgrsub2  44280  dflim5  44474  rp-fakeanorass  44657  mnuprdlem1  45399  mnuprdlem2  45400  mnurndlem1  45408  disjxp1  46228  fmul01lt1lem1  46738  stoweidlem35  47187  stirlinglem5  47230  stirlinglem12  47237  fourierdlem42  47301  fourierdlem93  47351  perfectALTVlem2  48962