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  2383  pwnss  5302  nsuceq0  6405  onssnel2i  6439  abnex  7713  ssonprc  7743  soseq  8115  dmtpos  8194  tfrlem15  8337  tz7.44-2  8352  tz7.48-3  8389  2pwuninel  9073  2pwne  9074  nnsdomg  9222  nnsdomgOLD  9223  r111  9704  r1pwss  9713  wfelirr  9754  rankxplim3  9810  carduni  9910  pr2neOLD  9934  alephle  10017  alephfp  10037  pwdjudom  10144  cfsuc  10186  fin23lem28  10269  fin23lem30  10271  isfin1-2  10314  ac5b  10407  zorn2lem4  10428  zorn2lem7  10431  cfpwsdom  10513  nd1  10516  nd2  10517  canthp1  10583  pwfseqlem1  10587  gchhar  10608  winalim2  10625  ltxrlt  11220  recgt0  12004  nnunb  12414  indstr  12851  wrdlen2i  14884  rlimno1  15596  lcmfnncl  16575  isprm2  16628  nprmdvds1  16652  divgcdodd  16656  coprm  16657  ramtcl2  16958  psgnunilem3  19402  torsubg  19760  prmcyg  19800  dprd2da  19950  prmirredlem  21358  pnfnei  23083  mnfnei  23084  1stccnp  23325  uzfbas  23761  ufinffr  23792  fin1aufil  23795  ovolunlem1a  25373  itg2gt0  25637  lgsquad2lem2  27272  dirith2  27415  noseponlem  27552  nosepssdm  27574  nodenselem8  27579  nolt02o  27583  nogt01o  27584  umgrnloop0  29012  usgrnloop0ALT  29108  nfrgr2v  30174  hon0  31695  ifeqeqx  32444  axsepg2ALT  35046  dfon2lem7  35750  bj-axc10v  36754  sbn1ALT  36819  bj-nsnid  37031  areacirclem4  37678  fdc  37712  dihglblem6  41307  sn-itrere  42449  sn-retire  42450  pellexlem6  42795  pw2f1ocnv  42999  wepwsolem  43004  inaex  44259  axc5c4c711toc5  44364  lptioo2  45602  lptioo1  45603  1neven  48199