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  2146  axc10  2417  pwnss  5320  nsuceq0  6474  onssnel2i  6507  abnex  7803  ssonprc  7835  soseq  8213  dmtpos  8293  tfrlem15  8438  tz7.44-2  8453  tz7.48-3  8492  2pwuninel  9189  2pwne  9190  nnsdomg  9329  r111  9819  r1pwss  9828  wfelirr  9871  rankxplim3  9935  carduni  10101  alephle  10206  alephfp  10226  pwdjudom  10332  cfsuc  10374  fin23lem28  10457  fin23lem30  10459  isfin1-2  10502  ac5b  10595  zorn2lem4  10616  zorn2lem7  10619  cfpwsdom  10708  nd1  10711  nd2  10712  canthp1  10778  pwfseqlem1  10782  gchhar  10803  winalim2  10820  ltxrlt  11419  recgt0  12203  nnunb  12642  indstr  13083  wrdlen2i  15136  rlimno1  15865  lcmfnncl  16848  isprm2  16901  nprmdvds1  16926  divgcdodd  16930  coprm  16931  ramtcl2  17233  chnccat  18850  psgnunilem3  19761  torsubg  20119  prmcyg  20159  dprd2da  20309  prmirredlem  21833  pnfnei  23593  mnfnei  23594  1stccnp  23836  uzfbas  24272  ufinffr  24303  fin1aufil  24306  ovolunlem1a  25872  itg2gt0  26136  lgsquad2lem2  27769  dirith2  27912  noseponlem  28078  nosepssdm  28100  nodenselem8  28105  nolt02o  28109  nogt01o  28110  umgrnloop0  29744  usgrnloop0ALT  29843  nfrgr2v  30930  hon0  32452  ifeqeqx  33236  rncardr1prc  35891  axsepg3ALT  35951  onprcf1acwevd  36088  dfon2lem7  36766  bj-axc10v  37920  sbn1ALT  37985  bj-nsnid  38255  areacirclem4  38897  fdc  38945  dihglblem6  42663  sn-itrere  43818  sn-retire  43819  pellexlem6  44107  pw2f1ocnv  44310  wepwsolem  44315  inaex  45542  axc5c4c711toc5  45647  lptioo2  46916  lptioo1  46917  1neven  49608