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  sbn1  2142  axc10  2417  pwnss  5322  nsuceq0  6446  onssnel2i  6479  abnex  7752  ssonprc  7782  soseq  8151  dmtpos  8230  tfrlem15  8375  tz7.44-2  8390  tz7.48-3  8427  2pwuninel  9116  2pwne  9117  nnsdomg  9255  r111  9743  r1pwss  9752  wfelirr  9793  rankxplim3  9849  carduni  9963  alephle  10068  alephfp  10088  pwdjudom  10194  cfsuc  10236  fin23lem28  10319  fin23lem30  10321  isfin1-2  10364  ac5b  10457  zorn2lem4  10478  zorn2lem7  10481  cfpwsdom  10564  nd1  10567  nd2  10568  canthp1  10634  pwfseqlem1  10638  gchhar  10659  winalim2  10676  ltxrlt  11275  recgt0  12056  nnunb  12495  indstr  12935  wrdlen2i  14975  rlimno1  15701  lcmfnncl  16682  isprm2  16735  nprmdvds1  16760  divgcdodd  16764  coprm  16765  ramtcl2  17066  chnccat  18677  psgnunilem3  19561  torsubg  19919  prmcyg  19959  dprd2da  20109  prmirredlem  21622  pnfnei  23377  mnfnei  23378  1stccnp  23619  uzfbas  24055  ufinffr  24086  fin1aufil  24089  ovolunlem1a  25655  itg2gt0  25919  lgsquad2lem2  27549  dirith2  27692  noseponlem  27828  nosepssdm  27850  nodenselem8  27855  nolt02o  27859  nogt01o  27860  umgrnloop0  29459  usgrnloop0ALT  29555  nfrgr2v  30623  hon0  32145  ifeqeqx  32888  axsepg3ALT  35555  dfon2lem7  36279  bj-axc10v  37428  sbn1ALT  37493  bj-nsnid  37706  areacirclem4  38362  fdc  38396  dihglblem6  42114  sn-itrere  43262  sn-retire  43263  pellexlem6  43561  pw2f1ocnv  43764  wepwsolem  43769  inaex  45007  axc5c4c711toc5  45112  lptioo2  46347  lptioo1  46348  1neven  49003