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  2143  axc10  2414  pwnss  5313  nsuceq0  6451  onssnel2i  6484  abnex  7775  ssonprc  7805  soseq  8183  dmtpos  8263  tfrlem15  8408  tz7.44-2  8423  tz7.48-3  8462  2pwuninel  9159  2pwne  9160  nnsdomg  9299  r111  9789  r1pwss  9798  wfelirr  9841  rankxplim3  9905  carduni  10069  alephle  10174  alephfp  10194  pwdjudom  10300  cfsuc  10342  fin23lem28  10425  fin23lem30  10427  isfin1-2  10470  ac5b  10563  zorn2lem4  10584  zorn2lem7  10587  cfpwsdom  10676  nd1  10679  nd2  10680  canthp1  10746  pwfseqlem1  10750  gchhar  10771  winalim2  10788  ltxrlt  11387  recgt0  12170  nnunb  12609  indstr  13050  wrdlen2i  15102  rlimno1  15830  lcmfnncl  16813  isprm2  16866  nprmdvds1  16891  divgcdodd  16895  coprm  16896  ramtcl2  17198  chnccat  18809  psgnunilem3  19719  torsubg  20077  prmcyg  20117  dprd2da  20267  prmirredlem  21787  pnfnei  23547  mnfnei  23548  1stccnp  23790  uzfbas  24226  ufinffr  24257  fin1aufil  24260  ovolunlem1a  25826  itg2gt0  26090  lgsquad2lem2  27721  dirith2  27864  noseponlem  28030  nosepssdm  28052  nodenselem8  28057  nolt02o  28061  nogt01o  28062  umgrnloop0  29696  usgrnloop0ALT  29795  nfrgr2v  30882  hon0  32404  ifeqeqx  33189  rncardr1prc  35826  axsepg3ALT  35878  onprcf1acwevd  35998  dfon2lem7  36675  bj-axc10v  37829  sbn1ALT  37894  bj-nsnid  38121  areacirclem4  38766  fdc  38816  dihglblem6  42534  sn-itrere  43689  sn-retire  43690  pellexlem6  43978  pw2f1ocnv  44181  wepwsolem  44186  inaex  45418  axc5c4c711toc5  45523  lptioo2  46779  lptioo1  46780  1neven  49471