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  5307  nsuceq0  6417  onssnel2i  6451  abnex  7733  ssonprc  7763  soseq  8138  dmtpos  8217  tfrlem15  8360  tz7.44-2  8375  tz7.48-3  8412  2pwuninel  9096  2pwne  9097  nnsdomg  9246  nnsdomgOLD  9247  r111  9728  r1pwss  9737  wfelirr  9778  rankxplim3  9834  carduni  9934  pr2neOLD  9958  alephle  10041  alephfp  10061  pwdjudom  10168  cfsuc  10210  fin23lem28  10293  fin23lem30  10295  isfin1-2  10338  ac5b  10431  zorn2lem4  10452  zorn2lem7  10455  cfpwsdom  10537  nd1  10540  nd2  10541  canthp1  10607  pwfseqlem1  10611  gchhar  10632  winalim2  10649  ltxrlt  11244  recgt0  12028  nnunb  12438  indstr  12875  wrdlen2i  14908  rlimno1  15620  lcmfnncl  16599  isprm2  16652  nprmdvds1  16676  divgcdodd  16680  coprm  16681  ramtcl2  16982  psgnunilem3  19426  torsubg  19784  prmcyg  19824  dprd2da  19974  prmirredlem  21382  pnfnei  23107  mnfnei  23108  1stccnp  23349  uzfbas  23785  ufinffr  23816  fin1aufil  23819  ovolunlem1a  25397  itg2gt0  25661  lgsquad2lem2  27296  dirith2  27439  noseponlem  27576  nosepssdm  27598  nodenselem8  27603  nolt02o  27607  nogt01o  27608  umgrnloop0  29036  usgrnloop0ALT  29132  nfrgr2v  30201  hon0  31722  ifeqeqx  32471  axsepg2ALT  35073  dfon2lem7  35777  bj-axc10v  36781  sbn1ALT  36846  bj-nsnid  37058  areacirclem4  37705  fdc  37739  dihglblem6  41334  sn-itrere  42476  sn-retire  42477  pellexlem6  42822  pw2f1ocnv  43026  wepwsolem  43031  inaex  44286  axc5c4c711toc5  44391  lptioo2  45629  lptioo1  45630  1neven  48226