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  2110  axc10  2385  pwnss  5288  nsuceq0  6391  onssnel2i  6424  abnex  7690  ssonprc  7720  soseq  8089  dmtpos  8168  tfrlem15  8311  tz7.44-2  8326  tz7.48-3  8363  2pwuninel  9045  2pwne  9046  nnsdomg  9183  r111  9668  r1pwss  9677  wfelirr  9718  rankxplim3  9774  carduni  9874  alephle  9979  alephfp  9999  pwdjudom  10106  cfsuc  10148  fin23lem28  10231  fin23lem30  10233  isfin1-2  10276  ac5b  10369  zorn2lem4  10390  zorn2lem7  10393  cfpwsdom  10475  nd1  10478  nd2  10479  canthp1  10545  pwfseqlem1  10549  gchhar  10570  winalim2  10587  ltxrlt  11183  recgt0  11967  nnunb  12377  indstr  12814  wrdlen2i  14849  rlimno1  15561  lcmfnncl  16540  isprm2  16593  nprmdvds1  16617  divgcdodd  16621  coprm  16622  ramtcl2  16923  chnccat  18532  psgnunilem3  19408  torsubg  19766  prmcyg  19806  dprd2da  19956  prmirredlem  21409  pnfnei  23135  mnfnei  23136  1stccnp  23377  uzfbas  23813  ufinffr  23844  fin1aufil  23847  ovolunlem1a  25424  itg2gt0  25688  lgsquad2lem2  27323  dirith2  27466  noseponlem  27603  nosepssdm  27625  nodenselem8  27630  nolt02o  27634  nogt01o  27635  umgrnloop0  29087  usgrnloop0ALT  29183  nfrgr2v  30252  hon0  31773  ifeqeqx  32522  axsepg2ALT  35095  dfon2lem7  35831  bj-axc10v  36837  sbn1ALT  36902  bj-nsnid  37114  areacirclem4  37761  fdc  37795  dihglblem6  41449  sn-itrere  42591  sn-retire  42592  pellexlem6  42937  pw2f1ocnv  43140  wepwsolem  43145  inaex  44400  axc5c4c711toc5  44505  lptioo2  45741  lptioo1  45742  1neven  48348