Theorem mtoi 190

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 189	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  2288  ssdifsn  4351  pwnss  4860  eunex  4889  nsuceq0  5843  onssnel2i  5876  abnex  7007  ssonprc  7034  reldmtpos  7405  dmtpos  7409  tfrlem15  7533  tz7.44-2  7548  tz7.48-3  7584  2pwuninel  8156  2pwne  8157  nnsdomg  8260  r111  8676  r1pwss  8685  wfelirr  8726  rankxplim3  8782  carduni  8845  pr2ne  8866  alephle  8949  alephfp  8969  pwcdadom  9076  cfsuc  9117  fin23lem28  9200  fin23lem30  9202  isfin1-2  9245  ac5b  9338  zorn2lem4  9359  zorn2lem7  9362  cfpwsdom  9444  nd1  9447  nd2  9448  canthp1  9514  pwfseqlem1  9518  gchhar  9539  winalim2  9556  ltxrlt  10146  recgt0  10905  nnunb  11326  indstr  11794  wrdlen2i  13732  rlimno1  14428  lcmfnncl  15389  isprm2  15442  nprmdvds1  15465  divgcdodd  15469  coprm  15470  ramtcl2  15762  psgnunilem3  17962  torsubg  18303  prmcyg  18341  dprd2da  18487  prmirredlem  19889  pnfnei  21072  mnfnei  21073  1stccnp  21313  uzfbas  21749  ufinffr  21780  fin1aufil  21783  ovolunlem1a  23310  itg2gt0  23572  lgsquad2lem2  25155  dirith2  25262  umgrnloop0  26049  usgrnloop0ALT  26142  nfrgr2v  27252  hon0  28780  ifeqeqx  29487  dfon2lem7  31818  soseq  31879  noseponlem  31942  nosepssdm  31961  nodenselem8  31966  nolt02o  31970  bj-axc10v  32842  bj-eunex  32924  areacirclem4  33633  fdc  33671  dihglblem6  36946  pellexlem6  37715  pw2f1ocnv  37921  wepwsolem  37929  axc5c4c711toc5  38920  lptioo2  40181  lptioo1  40182  1neven  42257