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  2108  axc10  2384  pwnss  5310  nsuceq0  6420  onssnel2i  6454  abnex  7736  ssonprc  7766  soseq  8141  dmtpos  8220  tfrlem15  8363  tz7.44-2  8378  tz7.48-3  8415  2pwuninel  9102  2pwne  9103  nnsdomg  9253  nnsdomgOLD  9254  r111  9735  r1pwss  9744  wfelirr  9785  rankxplim3  9841  carduni  9941  pr2neOLD  9965  alephle  10048  alephfp  10068  pwdjudom  10175  cfsuc  10217  fin23lem28  10300  fin23lem30  10302  isfin1-2  10345  ac5b  10438  zorn2lem4  10459  zorn2lem7  10462  cfpwsdom  10544  nd1  10547  nd2  10548  canthp1  10614  pwfseqlem1  10618  gchhar  10639  winalim2  10656  ltxrlt  11251  recgt0  12035  nnunb  12445  indstr  12882  wrdlen2i  14915  rlimno1  15627  lcmfnncl  16606  isprm2  16659  nprmdvds1  16683  divgcdodd  16687  coprm  16688  ramtcl2  16989  psgnunilem3  19433  torsubg  19791  prmcyg  19831  dprd2da  19981  prmirredlem  21389  pnfnei  23114  mnfnei  23115  1stccnp  23356  uzfbas  23792  ufinffr  23823  fin1aufil  23826  ovolunlem1a  25404  itg2gt0  25668  lgsquad2lem2  27303  dirith2  27446  noseponlem  27583  nosepssdm  27605  nodenselem8  27610  nolt02o  27614  nogt01o  27615  umgrnloop0  29043  usgrnloop0ALT  29139  nfrgr2v  30208  hon0  31729  ifeqeqx  32478  axsepg2ALT  35080  dfon2lem7  35784  bj-axc10v  36788  sbn1ALT  36853  bj-nsnid  37065  areacirclem4  37712  fdc  37746  dihglblem6  41341  sn-itrere  42483  sn-retire  42484  pellexlem6  42829  pw2f1ocnv  43033  wepwsolem  43038  inaex  44293  axc5c4c711toc5  44398  lptioo2  45636  lptioo1  45637  1neven  48230