Theorem mtoi 198

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 197	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  325  mtbiri  326  sbn1  2097  axc10  2378  pwnss  5351  nsuceq0  6454  onssnel2i  6488  abnex  7760  ssonprc  7791  soseq  8164  dmtpos  8244  tfrlem15  8413  tz7.44-2  8428  tz7.48-3  8465  2pwuninel  9157  2pwne  9158  nnsdomg  9327  nnsdomgOLD  9328  r111  9800  r1pwss  9809  wfelirr  9850  rankxplim3  9906  carduni  10006  pr2neOLD  10030  alephle  10113  alephfp  10133  pwdjudom  10241  cfsuc  10282  fin23lem28  10365  fin23lem30  10367  isfin1-2  10410  ac5b  10503  zorn2lem4  10524  zorn2lem7  10527  cfpwsdom  10609  nd1  10612  nd2  10613  canthp1  10679  pwfseqlem1  10683  gchhar  10704  winalim2  10721  ltxrlt  11316  recgt0  12093  nnunb  12501  indstr  12933  wrdlen2i  14929  rlimno1  15636  lcmfnncl  16603  isprm2  16656  nprmdvds1  16680  divgcdodd  16684  coprm  16685  ramtcl2  16983  psgnunilem3  19463  torsubg  19821  prmcyg  19861  dprd2da  20011  prmirredlem  21415  pnfnei  23168  mnfnei  23169  1stccnp  23410  uzfbas  23846  ufinffr  23877  fin1aufil  23880  ovolunlem1a  25469  itg2gt0  25734  lgsquad2lem2  27363  dirith2  27506  noseponlem  27643  nosepssdm  27665  nodenselem8  27670  nolt02o  27674  nogt01o  27675  umgrnloop0  28994  usgrnloop0ALT  29090  nfrgr2v  30154  hon0  31675  ifeqeqx  32412  dfon2lem7  35516  bj-axc10v  36401  sbn1ALT  36466  bj-nsnid  36680  areacirclem4  37315  fdc  37349  dihglblem6  40943  itrere  42014  sn-inelr  42155  sn-itrere  42156  sn-retire  42157  pellexlem6  42396  pw2f1ocnv  42600  wepwsolem  42608  inaex  43876  axc5c4c711toc5  43981  lptioo2  45157  lptioo1  45158  1neven  47486