Theorem mtoi 189

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 188	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  315  mtbiri  316  axc10  2240  pwnss  4756  eunex  4785  nsuceq0  5722  onssnel2i  5755  ssonprc  6884  reldmtpos  7247  dmtpos  7251  tfrlem15  7375  tz7.44-2  7390  tz7.48-3  7426  2pwuninel  8000  2pwne  8001  nnsdomg  8104  r111  8521  r1pwss  8530  wfelirr  8571  rankxplim3  8627  carduni  8690  pr2ne  8711  alephle  8794  alephfp  8814  pwcdadom  8921  cfsuc  8962  fin23lem28  9045  fin23lem30  9047  isfin1-2  9090  ac5b  9183  zorn2lem4  9204  zorn2lem7  9207  cfpwsdom  9285  nd1  9288  nd2  9289  canthp1  9355  pwfseqlem1  9359  gchhar  9380  winalim2  9397  ltxrlt  9987  recgt0  10746  nnunb  11165  indstr  11632  wrdlen2i  13534  rlimno1  14232  lcmfnncl  15180  isprm2  15233  nprmdvds1  15256  divgcdodd  15260  coprm  15261  ramtcl2  15553  psgnunilem3  17739  torsubg  18080  prmcyg  18118  dprd2da  18264  prmirredlem  19660  pnfnei  20834  mnfnei  20835  1stccnp  21075  uzfbas  21512  ufinffr  21543  fin1aufil  21546  ovolunlem1a  23071  itg2gt0  23333  lgsquad2lem2  24910  dirith2  25017  umgrnloop0  25775  usgranloop0  25909  nbgranself2  25965  frgra2v  26526  hon0  28036  ifeqeqx  28745  dfon2lem7  30938  soseq  30995  noseponlem  31065  nodenselem3  31082  nodenselem8  31087  bj-axc10v  31904  bj-eunex  31987  areacirclem4  32673  fdc  32711  dihglblem6  35647  pellexlem6  36416  pw2f1ocnv  36622  wepwsolem  36630  axc5c4c711toc5  37625  lptioo2  38698  lptioo1  38699  usgrnloop0ALT  40432  nfrgr2v  41442  1neven  41722  ssdifsn  42228