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  sbn1  2141  axc10  2416  pwnss  5308  nsuceq0  6431  onssnel2i  6464  abnex  7740  ssonprc  7770  soseq  8139  dmtpos  8218  tfrlem15  8363  tz7.44-2  8378  tz7.48-3  8415  2pwuninel  9104  2pwne  9105  nnsdomg  9243  r111  9733  r1pwss  9742  wfelirr  9783  rankxplim3  9839  carduni  9939  alephle  10044  alephfp  10064  pwdjudom  10171  cfsuc  10214  fin23lem28  10297  fin23lem30  10299  isfin1-2  10342  ac5b  10435  zorn2lem4  10456  zorn2lem7  10459  cfpwsdom  10542  nd1  10545  nd2  10546  canthp1  10612  pwfseqlem1  10616  gchhar  10637  winalim2  10654  ltxrlt  11253  recgt0  12037  nnunb  12477  indstr  12917  wrdlen2i  14955  rlimno1  15681  lcmfnncl  16663  isprm2  16716  nprmdvds1  16741  divgcdodd  16745  coprm  16746  ramtcl2  17047  chnccat  18658  psgnunilem3  19536  torsubg  19894  prmcyg  19934  dprd2da  20084  prmirredlem  21524  pnfnei  23280  mnfnei  23281  1stccnp  23522  uzfbas  23958  ufinffr  23989  fin1aufil  23992  ovolunlem1a  25558  itg2gt0  25822  lgsquad2lem2  27449  dirith2  27592  noseponlem  27728  nosepssdm  27750  nodenselem8  27755  nolt02o  27759  nogt01o  27760  umgrnloop0  29310  usgrnloop0ALT  29406  nfrgr2v  30474  hon0  31996  ifeqeqx  32741  axsepg3ALT  35438  dfon2lem7  36137  bj-axc10v  37278  sbn1ALT  37343  bj-nsnid  37555  areacirclem4  38210  fdc  38244  dihglblem6  41964  sn-itrere  43110  sn-retire  43111  pellexlem6  43411  pw2f1ocnv  43614  wepwsolem  43619  inaex  44873  axc5c4c711toc5  44978  lptioo2  46207  lptioo1  46208  1neven  48860