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  326  mtbiri  327  sbn1  2106  axc10  2386  pwnss  5273  nsuceq0  6350  onssnel2i  6381  abnex  7616  ssonprc  7646  dmtpos  8063  tfrlem15  8232  tz7.44-2  8247  tz7.48-3  8284  2pwuninel  8928  2pwne  8929  nnsdomg  9082  r111  9542  r1pwss  9551  wfelirr  9592  rankxplim3  9648  carduni  9748  pr2ne  9770  alephle  9853  alephfp  9873  pwdjudom  9981  cfsuc  10022  fin23lem28  10105  fin23lem30  10107  isfin1-2  10150  ac5b  10243  zorn2lem4  10264  zorn2lem7  10267  cfpwsdom  10349  nd1  10352  nd2  10353  canthp1  10419  pwfseqlem1  10423  gchhar  10444  winalim2  10461  ltxrlt  11054  recgt0  11830  nnunb  12238  indstr  12665  wrdlen2i  14664  rlimno1  15374  lcmfnncl  16343  isprm2  16396  nprmdvds1  16420  divgcdodd  16424  coprm  16425  ramtcl2  16721  psgnunilem3  19113  torsubg  19464  prmcyg  19504  dprd2da  19654  prmirredlem  20703  pnfnei  22380  mnfnei  22381  1stccnp  22622  uzfbas  23058  ufinffr  23089  fin1aufil  23092  ovolunlem1a  24669  itg2gt0  24934  lgsquad2lem2  26542  dirith2  26685  umgrnloop0  27488  usgrnloop0ALT  27581  nfrgr2v  28645  hon0  30164  ifeqeqx  30894  dfon2lem7  33774  soseq  33812  noseponlem  33876  nosepssdm  33898  nodenselem8  33903  nolt02o  33907  nogt01o  33908  bj-axc10v  34984  sbn1ALT  35051  bj-nsnid  35250  areacirclem4  35877  fdc  35912  dihglblem6  39361  sn-inelr  40442  itrere  40443  retire  40444  pellexlem6  40663  pw2f1ocnv  40866  wepwsolem  40874  inaex  41922  axc5c4c711toc5  42027  lptioo2  43179  lptioo1  43180  1neven  45501