Theorem mtoi 201

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 200	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  328  mtbiri  329  axc10  2402  pwnss  5253  nsuceq0  6274  onssnel2i  6304  abnex  7482  ssonprc  7510  dmtpos  7907  tfrlem15  8031  tz7.44-2  8046  tz7.48-3  8083  2pwuninel  8675  2pwne  8676  nnsdomg  8780  r111  9207  r1pwss  9216  wfelirr  9257  rankxplim3  9313  carduni  9413  pr2ne  9434  alephle  9517  alephfp  9537  pwdjudom  9641  cfsuc  9682  fin23lem28  9765  fin23lem30  9767  isfin1-2  9810  ac5b  9903  zorn2lem4  9924  zorn2lem7  9927  cfpwsdom  10009  nd1  10012  nd2  10013  canthp1  10079  pwfseqlem1  10083  gchhar  10104  winalim2  10121  ltxrlt  10714  recgt0  11489  nnunb  11896  indstr  12319  wrdlen2i  14307  rlimno1  15013  lcmfnncl  15976  isprm2  16029  nprmdvds1  16053  divgcdodd  16057  coprm  16058  ramtcl2  16350  psgnunilem3  18627  torsubg  18977  prmcyg  19017  dprd2da  19167  prmirredlem  20643  pnfnei  21831  mnfnei  21832  1stccnp  22073  uzfbas  22509  ufinffr  22540  fin1aufil  22543  ovolunlem1a  24100  itg2gt0  24364  lgsquad2lem2  25964  dirith2  26107  umgrnloop0  26897  usgrnloop0ALT  26990  nfrgr2v  28054  hon0  29573  ifeqeqx  30300  dfon2lem7  33038  soseq  33100  noseponlem  33175  nosepssdm  33194  nodenselem8  33199  nolt02o  33203  bj-axc10v  34119  bj-nsnid  34366  areacirclem4  34989  fdc  35024  dihglblem6  38480  sbn1  39108  pellexlem6  39437  pw2f1ocnv  39640  wepwsolem  39648  inaex  40639  axc5c4c711toc5  40740  lptioo2  41918  lptioo1  41919  1neven  44210