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

Theorem mtod 189
Description: Modus tollens deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
Hypotheses
Ref Expression
mtod.1 (𝜑 → ¬ 𝜒)
mtod.2 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
mtod (𝜑 → ¬ 𝜓)

Proof of Theorem mtod
StepHypRef Expression
1 mtod.2 . 2 (𝜑 → (𝜓𝜒))
2 mtod.1 . . 3 (𝜑 → ¬ 𝜒)
32a1d 25 . 2 (𝜑 → (𝜓 → ¬ 𝜒))
41, 3pm2.65d 187 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  mtoi  190  mtbid  315  mtbird  316  mtand  841  mtord  895  po2nr  5258  po3nr  5259  ordn2lp  5969  ordnbtwn  6040  fpropnf1  6757  tfi  7292  nnlim  7317  smoord  7707  tz7.48-3  7784  oalimcl  7886  omlimcl  7904  oneo  7907  omopth2  7910  nnneo  7977  mapdom2  8379  php3  8394  onomeneq  8398  sucdom2  8404  isfinite2  8466  domunfican  8481  ordtypelem7  8677  unxpwdom2  8741  cantnfp1lem2  8832  oemapvali  8837  cantnflem1  8842  cantnflem2  8843  rankpwi  8942  tskwe  9068  alephordi  9189  alephdom  9196  cardaleph  9204  cflim2  9379  isfin4-3  9431  fin23lem26  9441  fin1a2lem13  9528  axcclem  9573  fpwwe2lem12  9757  fpwwe2lem13  9758  fpwwe2  9759  pwxpndom2  9781  pwxpndom  9782  pwcdandom  9783  gchaleph  9787  r1wunlim  9853  inatsk  9894  tskuni  9899  gruina  9934  prlem934  10149  dedekind  10494  prodge0rd  12170  qextltlem  12270  ixxub  12433  ixxlb  12434  seqf1olem1  13082  facndiv  13314  cnpart  14222  rlimuni  14523  rlimcld2  14551  isercoll  14640  incexclem  14809  isumltss  14821  alzdvds  15284  fzm1ndvds  15286  fzo0dvdseq  15287  bitsfzolem  15394  smuval2  15442  smupvallem  15443  bezoutlem3  15496  rpdvds  15611  nonsq  15703  prmdiv  15726  odzdvds  15736  pcprendvds  15781  pcprendvds2  15782  pcpremul  15784  pcdvdsb  15809  pcadd2  15830  pockthlem  15845  prmreclem5  15860  prmreclem6  15861  1arith  15867  4sqlem11  15895  vdwlem11  15931  vdwlem12  15932  ramubcl  15958  mrissmrcd  16524  pltnlt  17192  acsfiindd  17401  odcl2  18202  gexnnod  18223  pgpssslw  18249  torsubg  18477  lt6abl  18516  ablfacrplem  18685  pgpfac1lem3  18697  irredrmul  18928  islbs3  19383  lbsextlem3  19388  lbsextlem4  19389  rng1nfld  19506  mvrf1  19653  f1lindf  20391  perfopn  21223  pnfnei  21258  mnfnei  21259  haust1  21390  cmpcld  21439  ptbasfi  21618  fbncp  21876  isfild  21895  fbasfip  21905  filufint  21957  rnelfmlem  21989  fmfnfm  21995  fclscf  22062  ptcmplem3  22091  opnsubg  22144  bldisj  22436  iccntr  22857  icccmplem2  22859  reconnlem1  22862  reconnlem2  22863  evth  22991  lebnumlem3  22995  ovolicc2lem3  23522  volfiniun  23550  iundisj  23551  dvne0  24010  lhop2  24014  itgsubstlem  24047  coemullem  24242  plyexmo  24304  logccne0  24561  lgamgulmlem1  24991  wilthlem2  25031  wilth  25033  mumul  25143  chtublem  25172  perfect1  25189  lgsdilem2  25294  lgsne0  25296  lgsqrlem2  25308  lgseisenlem1  25336  lgseisenlem2  25337  lgsquadlem1  25341  lgsquadlem2  25342  lgsquadlem3  25343  lgsquad2lem1  25345  2sqblem  25392  chebbnd1lem1  25394  pntpbnd2  25512  pntlem3  25534  ostth  25564  umgrnloop0  26240  usgrnloop0ALT  26334  wlkp1lem2  26821  pthdlem2lem  26913  chirredlem1  29599  iundisjf  29749  ofpreima2  29815  iundisjfi  29904  fundmpss  32007  dfon2lem4  32032  dfon2lem7  32035  sltval2  32151  nolt02o  32187  nosupbnd1lem2  32197  nosupbnd1  32202  nosupbnd2  32204  noetalem3  32207  broutsideof2  32571  outsidele  32581  nn0prpwlem  32659  nn0prpw  32660  onint1  32786  fin2so  33727  poimirlem16  33756  lpssat  34811  exatleN  35202  3noncolr2  35247  4noncolr3  35251  3dimlem3  35259  3dimlem3OLDN  35260  3dimlem4a  35261  3dimlem4  35262  3dimlem4OLDN  35263  3atlem4  35284  3atlem5  35285  3atlem6  35286  llnnleat  35311  lplnnle2at  35339  lvolnle3at  35380  4atlem0a  35391  4atlem0ae  35392  dalem21  35492  dalem54  35524  cdlemblem  35591  lhpmcvr4N  35824  4atexlemnclw  35868  cdlemd3  35998  cdleme3g  36032  cdleme3h  36033  cdleme7aa  36040  cdleme7d  36044  cdleme7ga  36046  cdleme11c  36059  cdleme15b  36073  cdleme20zN  36099  cdleme21b  36124  cdleme21c  36125  cdleme21ct  36127  cdleme22b  36139  cdleme32b  36240  cdleme35fnpq  36247  cdleme35f  36252  cdleme36a  36258  cdleme42c  36270  cdleme48bw  36300  cdlemf1  36359  cdlemg2fv2  36398  cdlemg7fvbwN  36405  cdlemg4  36415  cdlemg6c  36418  cdlemg27a  36490  cdlemg27b  36494  cdlemk3  36631  dia2dimlem1  36862  dihord6apre  37054  dihord6b  37058  dihord5apre  37060  dihglbcpreN  37098  dihmeetlem6  37107  dochnel2  37190  dochexmidlem7  37264  lspindp5  37568  mapdh8b  37578  hdmapip0  37713  pellexlem6  37917  elpell14qr2  37945  pellfundglb  37968  jm2.19  38078  jm2.26lem3  38086  setindtr  38109  harinf  38119  dgraa0p  38237  gneispace0nelrn3  38957
  Copyright terms: Public domain W3C validator