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  1918  elpwunsn  4645  disji2  5087  disjxiun  5100  pwssun  5543  swopo  5570  sotric  5589  sotrieq  5590  somo  5598  ordtri3or  6395  ordtri1  6396  suc11  6472  foconst  6811  ordeleqon  7796  ssonprc  7801  onmindif2  7821  limsssuc  7861  limom  7893  onfununi  8349  oeeulem  8610  uniinqs  8818  pw2f1olem  9100  pssnn  9184  ordtypelem9  9520  ordtypelem10  9521  oismo  9534  preleqALT  9618  suc11reg  9620  cantnfp1lem2  9680  cantnflem1  9690  cnfcom2lem  9702  cnfcom3lem  9704  rankxpsuc  9899  cardlim  10053  alephdom  10160  cardaleph  10168  iscard3  10172  pwdjudom  10293  cfslbn  10345  fin1a2lem12  10489  gchi  10709  tskssel  10842  inttsk  10859  inar1  10860  r1tskina  10867  tskuni  10868  gruina  10903  grur1  10905  nlt1pi  10991  nqereu  11014  leltne  11399  nneo  12783  zeo2  12786  xrleltne  13274  nltpnft  13294  ngtmnft  13296  xrrebnd  13298  xaddf  13354  xrsupsslem  13437  xrinfmsslem  13438  fzocatel  13864  seqf1olem1  14184  seqf1olem2  14185  znsqcld  14305  discr1  14383  hashnncl  14510  seqcoll2  14610  sgn3da  15254  sqeqd  15333  sqrmo  15418  isercoll  15835  bitsfzo  16605  bitsinv1lem  16611  bitsf1  16616  bezoutlem3  16714  eucalglt  16760  phibndlem  16947  dfphi2  16951  prmdiv  16962  odzdvds  16973  pceq0  17049  pc2dvds  17057  fldivp1  17075  pcfac  17077  prmreclem3  17096  1arith  17105  4sqlem10  17125  4sqlem17  17139  4sqlem18  17140  vdwlem6  17164  ramubcl  17196  ramcl  17207  mrissmrcd  17814  psgnunilem5  19708  oddvdsnn0  19758  odnncl  19759  oddvds  19761  odcl2  19779  gexdvds  19798  gexnnod  19802  sylow1lem1  19812  odcau  19818  pgpssslw  19828  efgs1b  19950  efgredlema  19954  torsubg  20068  prmcyg  20108  gsumval3eu  20118  ablfacrplem  20281  ablfac1eu  20289  ablsimpgprmd  20331  fidomndrnglem  21030  lspdisj  21403  lspsncv0  21424  prmidlc2  21630  gzrngunitlem  21738  prmirredlem  21778  fctop  23322  cctop  23324  ppttop  23325  pptbas  23326  ordtrest2lem  23521  connclo  23733  txindis  23953  filconn  24202  ufilb  24225  cldsubg  24430  reconnlem1  25146  reconnlem2  25147  metds0  25170  metdseq0  25174  metnrmlem1a  25178  iccpnfhmeo  25266  xrhmeo  25267  cphsubrglem  25498  minveclem3b  25749  minveclem4a  25751  vitalilem4  25932  itg2gt0  26081  itgsplitioo  26158  limccnp2  26212  rollelem  26309  dvlip  26313  itgsubstlem  26368  plyaddlem1  26532  plymullem1  26533  coefv0  26567  dgreq0  26584  radcnv0  26743  pserdvlem2  26755  pilem2  26779  sineq0  26852  logtayl  26988  cxpsqrt  27031  isosctrlem2  27147  atantayl2  27266  rlimcnp2  27294  amgm  27318  basellem3  27410  muval2  27461  sqf11  27466  chtnprm  27481  perfectlem2  27557  lgsdir  27659  lgsabs1  27663  lgseisenlem1  27702  2sqlem7  27751  2sqblem  27758  2sqmod  27763  2sqreultblem  27775  2sqreunnltblem  27778  chebbnd1lem1  27796  dchrisum0flblem1  27835  pntpbnd1  27913  pntpbnd2  27914  ostth  27966  nosepon  28022  abssge0  28631  elnns2  28727  dfnns2  28758  z12bday  28871  symquadlem  29161  midexlem  29164  colperp  29205  midex  29213  oppperpex  29229  hlpasch  29234  hpgerlem  29243  colopp  29247  plngrotlem1  29265  lmieu  29289  lmicom  29293  trgcopy  29311  cgracol  29336  minvecolem5  31483  staddi  32848  stadd3i  32850  atsseq  32949  atom1d  32955  atoml2i  32985  disji2f  33171  disjif2  33175  fprodex01  33416  psgnfzto1stlem  33661  lvecdim0  34239  ordtrest2NEWlem  34554  eulerpartlemb  35000  subfacp1lem6  35950  cvmscld  36038  cvmsss2  36039  cvmseu  36041  ordtoplem  37223  ordcmp  37235  poimirlem25  38563  heiborlem6  38750  isfldidl  39002  pridlc2  39006  mpobi123f  39094  mptbi12f  39098  ac6s6  39104  lsatcmp  40060  lsatcmp2  40061  2atm  40584  trlatn0  41229  trlval3  41244  cdleme18c  41350  cdlemg17b  41719  cdlemg17i  41726  cdlemh  41874  dia2dimlem2  42122  dia2dimlem3  42123  dochlkr  42442  dochkrshp  42443  lcfl6  42557  lcfrlem9  42607  hdmap14lem6  42930  hgmapval0  42949  ioin9i8  43259  ctbnfien  43824  pw2f1ocnv  44043  unxpwdom3  44096  dgrsub2  44136  dflim5  44330  rp-fakeanorass  44513  mnuprdlem1  45255  mnuprdlem2  45256  mnurndlem1  45264  disjxp1  46085  fmul01lt1lem1  46595  stoweidlem35  47044  stirlinglem5  47087  stirlinglem12  47094  fourierdlem42  47158  fourierdlem93  47208  perfectALTVlem2  48819