Theorem mtoi 200

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 199	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  327  mtbiri  328  sbn1  2118  axc10  2393  pwnss  5280  nsuceq0  6395  onssnel2i  6428  abnex  7700  ssonprc  7730  soseq  8099  dmtpos  8178  tfrlem15  8321  tz7.44-2  8336  tz7.48-3  8373  2pwuninel  9060  2pwne  9061  nnsdomg  9199  r111  9690  r1pwss  9699  wfelirr  9740  rankxplim3  9796  carduni  9896  alephle  10001  alephfp  10021  pwdjudom  10128  cfsuc  10170  fin23lem28  10253  fin23lem30  10255  isfin1-2  10298  ac5b  10391  zorn2lem4  10412  zorn2lem7  10415  cfpwsdom  10498  nd1  10501  nd2  10502  canthp1  10568  pwfseqlem1  10572  gchhar  10593  winalim2  10610  ltxrlt  11207  recgt0  11992  nnunb  12424  indstr  12857  wrdlen2i  14895  rlimno1  15607  lcmfnncl  16589  isprm2  16642  nprmdvds1  16667  divgcdodd  16671  coprm  16672  ramtcl2  16973  chnccat  18583  psgnunilem3  19462  torsubg  19820  prmcyg  19860  dprd2da  20010  prmirredlem  21447  pnfnei  23203  mnfnei  23204  1stccnp  23445  uzfbas  23881  ufinffr  23912  fin1aufil  23915  ovolunlem1a  25481  itg2gt0  25745  lgsquad2lem2  27366  dirith2  27509  noseponlem  27646  nosepssdm  27668  nodenselem8  27673  nolt02o  27677  nogt01o  27678  umgrnloop0  29196  usgrnloop0ALT  29292  nfrgr2v  30360  hon0  31882  ifeqeqx  32630  axsepg3ALT  35323  dfon2lem7  36015  bj-axc10v  37146  sbn1ALT  37211  bj-nsnid  37423  areacirclem4  38078  fdc  38112  dihglblem6  41832  sn-itrere  42978  sn-retire  42979  pellexlem6  43279  pw2f1ocnv  43482  wepwsolem  43487  inaex  44741  axc5c4c711toc5  44846  lptioo2  46076  lptioo1  46077  1neven  48729