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  2107  axc10  2389  pwnss  5322  nsuceq0  6436  onssnel2i  6470  abnex  7749  ssonprc  7779  soseq  8156  dmtpos  8235  tfrlem15  8404  tz7.44-2  8419  tz7.48-3  8456  2pwuninel  9144  2pwne  9145  nnsdomg  9305  nnsdomgOLD  9306  r111  9787  r1pwss  9796  wfelirr  9837  rankxplim3  9893  carduni  9993  pr2neOLD  10017  alephle  10100  alephfp  10120  pwdjudom  10227  cfsuc  10269  fin23lem28  10352  fin23lem30  10354  isfin1-2  10397  ac5b  10490  zorn2lem4  10511  zorn2lem7  10514  cfpwsdom  10596  nd1  10599  nd2  10600  canthp1  10666  pwfseqlem1  10670  gchhar  10691  winalim2  10708  ltxrlt  11303  recgt0  12085  nnunb  12495  indstr  12930  wrdlen2i  14959  rlimno1  15668  lcmfnncl  16646  isprm2  16699  nprmdvds1  16723  divgcdodd  16727  coprm  16728  ramtcl2  17029  psgnunilem3  19475  torsubg  19833  prmcyg  19873  dprd2da  20023  prmirredlem  21431  pnfnei  23156  mnfnei  23157  1stccnp  23398  uzfbas  23834  ufinffr  23865  fin1aufil  23868  ovolunlem1a  25447  itg2gt0  25711  lgsquad2lem2  27346  dirith2  27489  noseponlem  27626  nosepssdm  27648  nodenselem8  27653  nolt02o  27657  nogt01o  27658  umgrnloop0  29034  usgrnloop0ALT  29130  nfrgr2v  30199  hon0  31720  ifeqeqx  32469  axsepg2ALT  35060  dfon2lem7  35753  bj-axc10v  36757  sbn1ALT  36822  bj-nsnid  37034  areacirclem4  37681  fdc  37715  dihglblem6  41305  itrere  42314  sn-inelr  42457  sn-itrere  42458  sn-retire  42459  pellexlem6  42804  pw2f1ocnv  43008  wepwsolem  43013  inaex  44269  axc5c4c711toc5  44374  lptioo2  45608  lptioo1  45609  1neven  48161