Theorem mtoi 199

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 198	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  326  mtbiri  327  sbn1  2104  axc10  2387  pwnss  5357  nsuceq0  6468  onssnel2i  6502  abnex  7775  ssonprc  7806  soseq  8182  dmtpos  8261  tfrlem15  8430  tz7.44-2  8445  tz7.48-3  8482  2pwuninel  9170  2pwne  9171  nnsdomg  9332  nnsdomgOLD  9333  r111  9812  r1pwss  9821  wfelirr  9862  rankxplim3  9918  carduni  10018  pr2neOLD  10042  alephle  10125  alephfp  10145  pwdjudom  10252  cfsuc  10294  fin23lem28  10377  fin23lem30  10379  isfin1-2  10422  ac5b  10515  zorn2lem4  10536  zorn2lem7  10539  cfpwsdom  10621  nd1  10624  nd2  10625  canthp1  10691  pwfseqlem1  10695  gchhar  10716  winalim2  10733  ltxrlt  11328  recgt0  12110  nnunb  12519  indstr  12955  wrdlen2i  14977  rlimno1  15686  lcmfnncl  16662  isprm2  16715  nprmdvds1  16739  divgcdodd  16743  coprm  16744  ramtcl2  17044  psgnunilem3  19528  torsubg  19886  prmcyg  19926  dprd2da  20076  prmirredlem  21500  pnfnei  23243  mnfnei  23244  1stccnp  23485  uzfbas  23921  ufinffr  23952  fin1aufil  23955  ovolunlem1a  25544  itg2gt0  25809  lgsquad2lem2  27443  dirith2  27586  noseponlem  27723  nosepssdm  27745  nodenselem8  27750  nolt02o  27754  nogt01o  27755  umgrnloop0  29140  usgrnloop0ALT  29236  nfrgr2v  30300  hon0  31821  ifeqeqx  32562  axsepg2ALT  35075  dfon2lem7  35770  bj-axc10v  36775  sbn1ALT  36840  bj-nsnid  37052  areacirclem4  37697  fdc  37731  dihglblem6  41322  itrere  42331  sn-inelr  42473  sn-itrere  42474  sn-retire  42475  pellexlem6  42821  pw2f1ocnv  43025  wepwsolem  43030  inaex  44292  axc5c4c711toc5  44397  lptioo2  45586  lptioo1  45587  1neven  48081