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  2385  pwnss  5350  nsuceq0  6448  onssnel2i  6482  abnex  7744  ssonprc  7775  soseq  8145  dmtpos  8223  tfrlem15  8392  tz7.44-2  8407  tz7.48-3  8444  2pwuninel  9132  2pwne  9133  nnsdomg  9302  nnsdomgOLD  9303  r111  9770  r1pwss  9779  wfelirr  9820  rankxplim3  9876  carduni  9976  pr2neOLD  10000  alephle  10083  alephfp  10103  pwdjudom  10211  cfsuc  10252  fin23lem28  10335  fin23lem30  10337  isfin1-2  10380  ac5b  10473  zorn2lem4  10494  zorn2lem7  10497  cfpwsdom  10579  nd1  10582  nd2  10583  canthp1  10649  pwfseqlem1  10653  gchhar  10674  winalim2  10691  ltxrlt  11284  recgt0  12060  nnunb  12468  indstr  12900  wrdlen2i  14893  rlimno1  15600  lcmfnncl  16566  isprm2  16619  nprmdvds1  16643  divgcdodd  16647  coprm  16648  ramtcl2  16944  psgnunilem3  19364  torsubg  19722  prmcyg  19762  dprd2da  19912  prmirredlem  21042  pnfnei  22724  mnfnei  22725  1stccnp  22966  uzfbas  23402  ufinffr  23433  fin1aufil  23436  ovolunlem1a  25013  itg2gt0  25278  lgsquad2lem2  26888  dirith2  27031  noseponlem  27167  nosepssdm  27189  nodenselem8  27194  nolt02o  27198  nogt01o  27199  umgrnloop0  28369  usgrnloop0ALT  28462  nfrgr2v  29525  hon0  31046  ifeqeqx  31774  dfon2lem7  34761  bj-axc10v  35671  sbn1ALT  35737  bj-nsnid  35951  areacirclem4  36579  fdc  36613  dihglblem6  40211  sn-inelr  41338  itrere  41339  retire  41340  pellexlem6  41572  pw2f1ocnv  41776  wepwsolem  41784  inaex  43056  axc5c4c711toc5  43161  lptioo2  44347  lptioo1  44348  1neven  46830