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  2112  axc10  2389  pwnss  5297  nsuceq0  6402  onssnel2i  6435  abnex  7702  ssonprc  7732  soseq  8101  dmtpos  8180  tfrlem15  8323  tz7.44-2  8338  tz7.48-3  8375  2pwuninel  9060  2pwne  9061  nnsdomg  9199  r111  9687  r1pwss  9696  wfelirr  9737  rankxplim3  9793  carduni  9893  alephle  9998  alephfp  10018  pwdjudom  10125  cfsuc  10167  fin23lem28  10250  fin23lem30  10252  isfin1-2  10295  ac5b  10388  zorn2lem4  10409  zorn2lem7  10412  cfpwsdom  10495  nd1  10498  nd2  10499  canthp1  10565  pwfseqlem1  10569  gchhar  10590  winalim2  10607  ltxrlt  11203  recgt0  11987  nnunb  12397  indstr  12829  wrdlen2i  14865  rlimno1  15577  lcmfnncl  16556  isprm2  16609  nprmdvds1  16633  divgcdodd  16637  coprm  16638  ramtcl2  16939  chnccat  18549  psgnunilem3  19425  torsubg  19783  prmcyg  19823  dprd2da  19973  prmirredlem  21427  pnfnei  23164  mnfnei  23165  1stccnp  23406  uzfbas  23842  ufinffr  23873  fin1aufil  23876  ovolunlem1a  25453  itg2gt0  25717  lgsquad2lem2  27352  dirith2  27495  noseponlem  27632  nosepssdm  27654  nodenselem8  27659  nolt02o  27663  nogt01o  27664  umgrnloop0  29182  usgrnloop0ALT  29278  nfrgr2v  30347  hon0  31868  ifeqeqx  32617  axsepg2ALT  35239  dfon2lem7  35981  bj-axc10v  36994  sbn1ALT  37059  bj-nsnid  37271  areacirclem4  37912  fdc  37946  dihglblem6  41600  sn-itrere  42743  sn-retire  42744  pellexlem6  43076  pw2f1ocnv  43279  wepwsolem  43284  inaex  44538  axc5c4c711toc5  44643  lptioo2  45877  lptioo1  45878  1neven  48484