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  2144  axc10  2415  pwnss  5313  nsuceq0  6448  onssnel2i  6481  abnex  7771  ssonprc  7801  soseq  8176  dmtpos  8255  tfrlem15  8400  tz7.44-2  8415  tz7.48-3  8454  2pwuninel  9151  2pwne  9152  nnsdomg  9291  r111  9782  r1pwss  9791  wfelirr  9834  rankxplim3  9898  carduni  10062  alephle  10167  alephfp  10187  pwdjudom  10293  cfsuc  10335  fin23lem28  10418  fin23lem30  10420  isfin1-2  10463  ac5b  10556  zorn2lem4  10577  zorn2lem7  10580  cfpwsdom  10669  nd1  10672  nd2  10673  canthp1  10739  pwfseqlem1  10743  gchhar  10764  winalim2  10781  ltxrlt  11380  recgt0  12163  nnunb  12602  indstr  13043  wrdlen2i  15093  rlimno1  15821  lcmfnncl  16804  isprm2  16857  nprmdvds1  16882  divgcdodd  16886  coprm  16887  ramtcl2  17189  chnccat  18800  psgnunilem3  19710  torsubg  20068  prmcyg  20108  dprd2da  20258  prmirredlem  21778  pnfnei  23538  mnfnei  23539  1stccnp  23781  uzfbas  24217  ufinffr  24248  fin1aufil  24251  ovolunlem1a  25817  itg2gt0  26081  lgsquad2lem2  27712  dirith2  27855  noseponlem  28021  nosepssdm  28043  nodenselem8  28048  nolt02o  28052  nogt01o  28053  umgrnloop0  29687  usgrnloop0ALT  29786  nfrgr2v  30873  hon0  32395  ifeqeqx  33138  rncardr1prc  35758  axsepg3ALT  35810  onprcf1acwevd  35897  dfon2lem7  36551  bj-axc10v  37705  sbn1ALT  37770  bj-nsnid  37985  areacirclem4  38629  fdc  38679  dihglblem6  42397  sn-itrere  43552  sn-retire  43553  pellexlem6  43840  pw2f1ocnv  44043  wepwsolem  44048  inaex  45280  axc5c4c711toc5  45385  lptioo2  46642  lptioo1  46643  1neven  49334