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 ⊢ (𝜑 → ¬ 𝜓)

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:  mtbii  329  mtbiri  330  sbn1  2145  axc10  2419  pwnss  5324  nsuceq0  6450  onssnel2i  6483  abnex  7762  ssonprc  7792  soseq  8161  dmtpos  8240  tfrlem15  8385  tz7.44-2  8400  tz7.48-3  8437  2pwuninel  9127  2pwne  9128  nnsdomg  9266  r111  9754  r1pwss  9763  wfelirr  9804  rankxplim3  9860  carduni  9983  alephle  10088  alephfp  10108  pwdjudom  10214  cfsuc  10256  fin23lem28  10339  fin23lem30  10341  isfin1-2  10384  ac5b  10477  zorn2lem4  10498  zorn2lem7  10501  cfpwsdom  10584  nd1  10587  nd2  10588  canthp1  10654  pwfseqlem1  10658  gchhar  10679  winalim2  10696  ltxrlt  11295  recgt0  12076  nnunb  12515  indstr  12956  wrdlen2i  15003  rlimno1  15729  lcmfnncl  16709  isprm2  16762  nprmdvds1  16787  divgcdodd  16791  coprm  16792  ramtcl2  17093  chnccat  18704  psgnunilem3  19610  torsubg  19968  prmcyg  20008  dprd2da  20158  prmirredlem  21672  pnfnei  23427  mnfnei  23428  1stccnp  23670  uzfbas  24106  ufinffr  24137  fin1aufil  24140  ovolunlem1a  25706  itg2gt0  25970  lgsquad2lem2  27600  dirith2  27743  noseponlem  27879  nosepssdm  27901  nodenselem8  27906  nolt02o  27910  nogt01o  27911  umgrnloop0  29514  usgrnloop0ALT  29613  nfrgr2v  30694  hon0  32216  ifeqeqx  32959  axsepg3ALT  35612  dfon2lem7  36316  bj-axc10v  37485  sbn1ALT  37550  bj-nsnid  37763  areacirclem4  38419  fdc  38454  dihglblem6  42172  sn-itrere  43320  sn-retire  43321  pellexlem6  43619  pw2f1ocnv  43822  wepwsolem  43827  inaex  45065  axc5c4c711toc5  45170  lptioo2  46405  lptioo1  46406  1neven  49060