MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ord Structured version   Visualization version   GIF version

Theorem ord 392
Description: Deduce implication from disjunction. (Contributed by NM, 18-May-1994.)
Hypothesis
Ref Expression
ord.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
ord (𝜑 → (¬ 𝜓𝜒))

Proof of Theorem ord
StepHypRef Expression
1 ord.1 . 2 (𝜑 → (𝜓𝜒))
2 df-or 385 . 2 ((𝜓𝜒) ↔ (¬ 𝜓𝜒))
31, 2sylib 208 1 (𝜑 → (¬ 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 383
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 197  df-or 385
This theorem is referenced by:  ornld  939  orcanai  951  oplem1  1006  ecase23d  1434  19.33b  1811  elpwunsn  4215  eqsnOLD  4353  disji2  4627  disjxiun  4640  disjxiunOLD  4641  pwssun  5010  swopo  5035  sotric  5051  sotrieq  5052  somo  5059  ordtri3or  5743  ordtri1  5744  ordtri3OLD  5748  suc11  5819  foconst  6113  ordeleqon  6973  ssonprc  6977  onmindif2  6997  limsssuc  7035  limom  7065  onfununi  7423  oeeulem  7666  uniinqs  7812  pw2f1olem  8049  pssnn  8163  ordtypelem9  8416  ordtypelem10  8417  oismo  8430  preleq  8499  suc11reg  8501  cantnfp1lem2  8561  cantnflem1  8571  cnfcom2lem  8583  cnfcom3lem  8585  rankxpsuc  8730  cardlim  8783  alephdom  8889  cardaleph  8897  iscard3  8901  pwcdadom  9023  cfslbn  9074  fin1a2lem12  9218  gchi  9431  fpwwe2lem13  9449  tskssel  9564  inttsk  9581  inar1  9582  r1tskina  9589  tskuni  9590  gruina  9625  grur1  9627  nlt1pi  9713  nqereu  9736  leltne  10112  nneo  11446  zeo2  11449  xrleltne  11963  nltpnft  11980  ngtmnft  11982  xrrebnd  11984  xaddf  12040  xrsupsslem  12122  xrinfmsslem  12123  fzocatel  12515  seqf1olem1  12823  seqf1olem2  12824  discr1  12983  hashnncl  13140  seqcoll2  13232  sqeqd  13887  sqrmo  13973  isercoll  14379  bitsfzo  15138  bitsinv1lem  15144  bitsf1  15149  bezoutlem3  15239  eucalglt  15279  phibndlem  15456  dfphi2  15460  prmdiv  15471  odzdvds  15481  pceq0  15556  pc2dvds  15564  fldivp1  15582  pcfac  15584  prmreclem3  15603  1arith  15612  4sqlem10  15632  4sqlem17  15646  4sqlem18  15647  vdwlem6  15671  ramubcl  15703  ramcl  15714  mrissmrcd  16281  psgnunilem5  17895  oddvdsnn0  17944  odnncl  17945  oddvds  17947  odcl2  17963  gexdvds  17980  gexnnod  17984  sylow1lem1  17994  odcau  18000  pgpssslw  18010  efgs1b  18130  efgredlema  18134  torsubg  18238  prmcyg  18276  gsumval3eu  18286  ablfacrplem  18445  ablfac1eu  18453  lspdisj  19106  lspsncv0  19127  fidomndrnglem  19287  gzrngunitlem  19792  prmirredlem  19822  fctop  20789  cctop  20791  ppttop  20792  pptbas  20793  ordtrest2lem  20988  connclo  21199  txindis  21418  filconn  21668  ufilb  21691  cldsubg  21895  reconnlem1  22610  reconnlem2  22611  metds0  22634  metdseq0  22638  metnrmlem1a  22642  iccpnfhmeo  22725  xrhmeo  22726  cphsubrglem  22958  minveclem3b  23180  minveclem4a  23182  vitalilem4  23361  itg2gt0  23508  itgsplitioo  23585  limccnp2  23637  rollelem  23733  dvlip  23737  itgsubstlem  23792  plyaddlem1  23950  plymullem1  23951  coefv0  23985  dgreq0  24002  radcnv0  24151  pserdvlem2  24163  pilem2  24187  sineq0  24254  logtayl  24387  cxpsqrt  24430  isosctrlem2  24530  atantayl2  24646  leibpilem1  24648  rlimcnp2  24674  amgm  24698  basellem3  24790  muval2  24841  sqf11  24846  ppinprm  24859  chtnprm  24861  perfectlem2  24936  lgsdir  25038  lgsabs1  25042  lgseisenlem1  25081  2sqlem7  25130  2sqblem  25137  chebbnd1lem1  25139  dchrisum0flblem1  25178  pntpbnd1  25256  pntpbnd2  25257  ostth  25309  symquadlem  25565  midexlem  25568  colperp  25602  midex  25610  oppperpex  25626  outpasch  25628  hlpasch  25629  hpgerlem  25638  colopp  25642  colhp  25643  lmieu  25657  lmicom  25661  trgcopy  25677  cgracol  25700  minvecolem5  27707  staddi  29075  stadd3i  29077  atsseq  29176  atom1d  29182  atoml2i  29212  disji2f  29362  disjif2  29366  znsqcld  29486  fprodex01  29545  2sqmod  29622  psgnfzto1stlem  29824  ordtrest2NEWlem  29942  eulerpartlemb  30404  sgn3da  30577  subfacp1lem6  31141  cvmscld  31229  cvmsss2  31230  cvmseu  31232  nosepon  31792  ordtoplem  32409  ordcmp  32421  poimirlem25  33405  heiborlem6  33586  isfldidl  33838  pridlc2  33842  mpt2bi123f  33942  mptbi12f  33946  ac6s6  33951  lsatcmp  34109  lsatcmp2  34110  2atm  34632  trlatn0  35278  trlval3  35293  cdleme18c  35399  cdlemg17b  35769  cdlemg17i  35776  cdlemh  35924  dia2dimlem2  36173  dia2dimlem3  36174  dochlkr  36493  dochkrshp  36494  lcfl6  36608  lcfrlem9  36658  hdmap14lem6  36984  hgmapval0  37003  ctbnfien  37201  pw2f1ocnv  37423  unxpwdom3  37484  dgrsub2  37524  rp-fakeanorass  37677  disjxp1  39058  fmul01lt1lem1  39616  elprn1  39665  stoweidlem35  40015  stirlinglem5  40058  stirlinglem12  40065  fourierdlem42  40129  fourierdlem93  40179  perfectALTVlem2  41396
  Copyright terms: Public domain W3C validator