Theorem mtoi 202

Description: Modus tollens inference. (Contributed by NM, 5-Jul-1994.) (Proof shortened by Wolf Lammen, 15-Sep-2012.)

Hypotheses

Ref	Expression
mtoi.1	⊢ ¬ 𝜒
mtoi.2	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
mtoi	⊢ (𝜑 → ¬ 𝜓)

Proof of Theorem mtoi

Step	Hyp	Ref	Expression
1		mtoi.1	. . 3 ⊢ ¬ 𝜒
2	1	a1i 11	. 2 ⊢ (𝜑 → ¬ 𝜒)
3		mtoi.2	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	mtod 201	1 ⊢ (𝜑 → ¬ 𝜓)

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:  mtbii  329  mtbiri  330  axc10  2392  pwnss  5215  nsuceq0  6239  onssnel2i  6269  abnex  7459  ssonprc  7487  dmtpos  7887  tfrlem15  8011  tz7.44-2  8026  tz7.48-3  8063  2pwuninel  8656  2pwne  8657  nnsdomg  8761  r111  9188  r1pwss  9197  wfelirr  9238  rankxplim3  9294  carduni  9394  pr2ne  9416  alephle  9499  alephfp  9519  pwdjudom  9627  cfsuc  9668  fin23lem28  9751  fin23lem30  9753  isfin1-2  9796  ac5b  9889  zorn2lem4  9910  zorn2lem7  9913  cfpwsdom  9995  nd1  9998  nd2  9999  canthp1  10065  pwfseqlem1  10069  gchhar  10090  winalim2  10107  ltxrlt  10700  recgt0  11475  nnunb  11881  indstr  12304  wrdlen2i  14295  rlimno1  15002  lcmfnncl  15963  isprm2  16016  nprmdvds1  16040  divgcdodd  16044  coprm  16045  ramtcl2  16337  psgnunilem3  18616  torsubg  18967  prmcyg  19007  dprd2da  19157  prmirredlem  20186  pnfnei  21825  mnfnei  21826  1stccnp  22067  uzfbas  22503  ufinffr  22534  fin1aufil  22537  ovolunlem1a  24100  itg2gt0  24364  lgsquad2lem2  25969  dirith2  26112  umgrnloop0  26902  usgrnloop0ALT  26995  nfrgr2v  28057  hon0  29576  ifeqeqx  30309  dfon2lem7  33147  soseq  33209  noseponlem  33284  nosepssdm  33303  nodenselem8  33308  nolt02o  33312  bj-axc10v  34230  bj-nsnid  34486  areacirclem4  35148  fdc  35183  dihglblem6  38636  sbn1  39394  sn-inelr  39590  itrere  39591  retire  39592  pellexlem6  39775  pw2f1ocnv  39978  wepwsolem  39986  inaex  41005  axc5c4c711toc5  41106  lptioo2  42273  lptioo1  42274  1neven  44556