Theorem mtod 201

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

Step	Hyp	Ref	Expression
1		mtod.2	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		mtod.1	. . 3 ⊢ (𝜑 → ¬ 𝜒)
3	2	a1d 26	. 2 ⊢ (𝜑 → (𝜓 → ¬ 𝜒))
4	1, 3	pm2.65d 199	1 ⊢ (𝜑 → ¬ 𝜓)

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  mtoi  202  mtbid  327  mtbird  328  mtand  828  mtord  893  nrmod  3839  po2nr  5573  po3nr  5574  ordn2lp  6383  ordnbtwn  6459  fpropnf1  7272  tfi  7865  nnlim  7892  frrlem14  8318  smoord  8374  tz7.48-3  8455  oalimcl  8569  omlimcl  8587  oneo  8590  omopth2  8593  nnneo  8665  mapdom2  9168  sucdom2  9219  php2  9224  1sdom2dom  9246  isfinite2  9291  domunfican  9314  ordtypelem7  9519  unxpwdom2  9583  cantnfp1lem2  9681  oemapvali  9686  cantnflem1  9691  cantnflem2  9692  rankpwi  9833  tskwe  10032  alephordi  10154  alephdom  10161  cardaleph  10169  cflim2  10342  isfin4p1  10394  fin23lem26  10404  fin1a2lem13  10491  axcclem  10536  fpwwe2lem11  10727  fpwwe2lem12  10728  fpwwe2  10729  pwxpndom2  10751  pwxpndom  10752  pwdjundom  10753  gchaleph  10757  r1wunlim  10823  inatsk  10864  tskuni  10869  gruina  10904  prlem934  11119  dedekind  11474  prodge0rd  13230  qextltlem  13333  ixxub  13498  ixxlb  13499  seqf1olem1  14185  facndiv  14433  cnpart  15408  rlimuni  15718  rlimcld2  15746  isercoll  15836  incexclem  16006  isumltss  16018  alzdvds  16491  fzm1ndvds  16493  fzo0dvdseq  16494  bitsfzolem  16605  smuval2  16653  smupvallem  16654  bezoutlem3  16715  rpdvds  16836  nonsq  16936  prmdiv  16963  odzdvds  16974  pcprendvds  17019  pcprendvds2  17020  pcpremul  17022  pcdvdsb  17048  pcadd2  17069  pockthlem  17084  prmreclem5  17099  prmreclem6  17100  1arith  17106  4sqlem11  17134  vdwlem11  17170  vdwlem12  17171  ramubcl  17197  mrissmrcd  17815  pltnlt  18513  acsfiindd  18728  odcl2  19780  gexnnod  19803  pgpssslw  19829  torsubg  20069  lt6abl  20110  ablfacrplem  20282  pgpfac1lem3  20294  ablsimpnosubgd  20321  irredrmul  20658  islbs3  21434  lbsextlem3  21439  lbsextlem4  21440  f1lindf  22129  mvrf1  22294  psdmul  22488  perfopn  23504  pnfnei  23539  mnfnei  23540  haust1  23671  cmpcld  23721  ptbasfi  23901  fbncp  24159  isfild  24178  fbasfip  24188  filufint  24240  rnelfmlem  24272  fmfnfm  24278  fclscf  24345  ptcmplem3  24374  opnsubg  24428  bldisj  24718  iccntr  25142  icccmplem2  25144  reconnlem1  25147  reconnlem2  25148  evth  25281  lebnumlem3  25285  ovolicc2lem3  25841  volfiniun  25869  iundisj  25870  dvne0  26332  lhop2  26336  itgsubstlem  26369  coemullem  26570  rnplynfin  26631  plyexmo  26637  logccne0  26907  rtprmirr  27089  lgamgulmlem1  27357  wilthlem2  27397  wilth  27399  mumul  27509  chtublem  27539  perfect1  27556  lgsdilem2  27661  lgsne0  27663  lgsqrlem2  27675  lgseisenlem1  27703  lgseisenlem2  27704  lgsquadlem1  27708  lgsquadlem2  27709  lgsquadlem3  27710  lgsquad2lem1  27712  2sqblem  27759  chebbnd1lem1  27797  pntpbnd2  27915  pntlem3  27937  ostth  27967  flt4lem5elem  27982  flt4lem7  27990  nna4b4nsq  27991  ltsval2  28014  nolt02o  28053  nosupbnd1lem2  28067  nosupbnd1  28072  nosupbnd2  28074  noinfbnd1lem2  28082  noinfbnd1  28087  noinfbnd2  28089  noetasuplem4  28094  noetainflem4  28098  cutbdaybnd2lim  28184  oniso  28658  bdayfinbndlem1  28854  z12bdaylem1  28857  umgrnloop0  29688  usgrnloop0ALT  29787  wlkp1lem2  30254  pthdlem2lem  30354  chirredlem1  32993  iundisjf  33184  ofpreima2  33261  iundisjfi  33389  rprmndvdsru  34062  acwer1prc  35761  vonf1onprcf1ac  35895  onprcf1acwevd  35898  antnest  36455  antnestlaw3lem  36456  fundmpss  36533  dfon2lem4  36549  dfon2lem7  36552  broutsideof2  36888  outsidele  36898  nn0prpwlem  37111  onint1  37238  fin2so  38532  lindsadd  38538  suceldisj  39752  lpssat  40072  exatleN  40463  3noncolr2  40508  4noncolr3  40512  3dimlem3  40520  3dimlem3OLDN  40521  3dimlem4a  40522  3dimlem4  40523  3dimlem4OLDN  40524  3atlem4  40545  3atlem5  40546  3atlem6  40547  llnnleat  40572  lplnnle2at  40600  lvolnle3at  40641  4atlem0a  40652  4atlem0ae  40653  dalem21  40753  dalem54  40785  cdlemblem  40852  lhpmcvr4N  41085  4atexlemnclw  41129  cdlemd3  41259  cdleme3g  41293  cdleme3h  41294  cdleme7aa  41301  cdleme7d  41305  cdleme7ga  41307  cdleme11c  41320  cdleme15b  41334  cdleme20zN  41360  cdleme21b  41385  cdleme21c  41386  cdleme21ct  41388  cdleme22b  41400  cdleme32b  41501  cdleme35fnpq  41508  cdleme35f  41513  cdleme36a  41519  cdleme42c  41531  cdleme48bw  41561  cdlemf1  41620  cdlemg2fv2  41659  cdlemg7fvbwN  41666  cdlemg4  41676  cdlemg6c  41679  cdlemg27a  41751  cdlemg27b  41755  cdlemk3  41892  dia2dimlem1  42123  dihord6apre  42315  dihord6b  42319  dihord5apre  42321  dihglbcpreN  42359  dihmeetlem6  42368  dochnel2  42451  dochexmidlem7  42525  lspindp5  42829  mapdh8b  42839  hdmapip0  42974  aks6d1c2p2  43171  pellexlem6  43842  elpell14qr2  43870  pellfundglb  43893  jm2.19  44001  jm2.26lem3  44009  setindtr  44032  harinf  44042  dgraa0p  44152  tfsconcatb0  44347  gneispace0nelrn3  45143  nellindf  50971