Theorem mtoi 198

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 197	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  325  mtbiri  326  sbn1  2107  axc10  2385  pwnss  5267  nsuceq0  6331  onssnel2i  6362  abnex  7585  ssonprc  7614  dmtpos  8025  tfrlem15  8194  tz7.44-2  8209  tz7.48-3  8245  2pwuninel  8868  2pwne  8869  nnsdomg  9003  r111  9464  r1pwss  9473  wfelirr  9514  rankxplim3  9570  carduni  9670  pr2ne  9692  alephle  9775  alephfp  9795  pwdjudom  9903  cfsuc  9944  fin23lem28  10027  fin23lem30  10029  isfin1-2  10072  ac5b  10165  zorn2lem4  10186  zorn2lem7  10189  cfpwsdom  10271  nd1  10274  nd2  10275  canthp1  10341  pwfseqlem1  10345  gchhar  10366  winalim2  10383  ltxrlt  10976  recgt0  11751  nnunb  12159  indstr  12585  wrdlen2i  14583  rlimno1  15293  lcmfnncl  16262  isprm2  16315  nprmdvds1  16339  divgcdodd  16343  coprm  16344  ramtcl2  16640  psgnunilem3  19019  torsubg  19370  prmcyg  19410  dprd2da  19560  prmirredlem  20606  pnfnei  22279  mnfnei  22280  1stccnp  22521  uzfbas  22957  ufinffr  22988  fin1aufil  22991  ovolunlem1a  24565  itg2gt0  24830  lgsquad2lem2  26438  dirith2  26581  umgrnloop0  27382  usgrnloop0ALT  27475  nfrgr2v  28537  hon0  30056  ifeqeqx  30786  dfon2lem7  33671  soseq  33730  noseponlem  33794  nosepssdm  33816  nodenselem8  33821  nolt02o  33825  nogt01o  33826  bj-axc10v  34902  sbn1ALT  34969  bj-nsnid  35168  areacirclem4  35795  fdc  35830  dihglblem6  39281  sn-inelr  40356  itrere  40357  retire  40358  pellexlem6  40572  pw2f1ocnv  40775  wepwsolem  40783  inaex  41804  axc5c4c711toc5  41909  lptioo2  43062  lptioo1  43063  1neven  45378