Theorem mto 199

Description: The rule of modus tollens. The rule says, "if 𝜓 is not true, and 𝜑 implies 𝜓, then 𝜑 must also be not true". Modus tollens is short for "modus tollendo tollens", a Latin phrase that means "the mode that by denying denies" - remark in [Sanford] p. 39. It is also called denying the consequent. Modus tollens is closely related to modus ponens ax-mp 5. Note that this rule is also valid in intuitionistic logic. Inference associated with con3i 157. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)

Hypotheses

Ref	Expression
mto.1	⊢ ¬ 𝜓
mto.2	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
mto	⊢ ¬ 𝜑

Proof of Theorem mto

Step	Hyp	Ref	Expression
1		mto.2	. 2 ⊢ (𝜑 → 𝜓)
2		mto.1	. . 3 ⊢ ¬ 𝜓
3	2	a1i 11	. 2 ⊢ (𝜑 → ¬ 𝜓)
4	1, 3	pm2.65i 196	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:  mt3  203  mtbi  324  intnan  489  intnanr  490  pm3.2ni  877  nexr  2191  nonconne  3030  ru  3773  noel  4298  reu0  4320  neldifsn  4727  axnulALT  5210  nvel  5222  nfnid  5278  nprrel  5613  0xp  5651  son2lpi  5990  nlim0  6251  snsn0non  6311  nfunv  6390  dffv3  6668  mpo0  7241  onprc  7501  ordeleqon  7505  onuninsuci  7557  orduninsuc  7560  iprc  7620  tfrlem13  8028  tfrlem14  8029  tfrlem16  8031  tfr2b  8034  tz7.44lem1  8043  sdomn2lp  8658  canth2  8672  map2xp  8689  fi0  8886  sucprcreg  9067  rankxplim3  9312  alephnbtwn2  9500  alephprc  9527  unialeph  9529  kmlem16  9593  cfsuc  9681  nd1  10011  nd2  10012  canthp1lem2  10077  0nnq  10348  1ne0sr  10520  pnfnre  10684  mnfnre  10686  ine0  11077  recgt0ii  11548  inelr  11630  0nnn  11676  nnunb  11896  nn0nepnf  11978  indstr  12319  1nuz2  12327  0nrp  12427  lsw0  13919  egt2lt3  15561  ruc  15598  odd2np1  15692  n2dvds1OLD  15720  divalglem5  15750  bitsf1  15797  0nprm  16024  structcnvcnv  16499  fvsetsid  16517  fnpr2ob  16833  oduclatb  17756  0g0  17876  psgnunilem3  18626  00ply1bas  20410  zringndrg  20639  0ntop  21515  topnex  21606  bwth  22020  ustn0  22831  vitalilem5  24215  deg1nn0clb  24686  aaliou3lem9  24941  sinhalfpilem  25051  logdmn0  25225  dvlog  25236  ppiltx  25756  dchrisum0fno1  26089  axlowdim1  26747  topnfbey  28250  0ngrp  28290  dmadjrnb  29685  neldifpr1  30295  neldifpr2  30296  1nei  30474  nn0xmulclb  30498  ballotlem2  31748  bnj521  32009  bnj1304  32093  bnj110  32132  bnj98  32141  bnj1523  32345  subfacp1lem5  32433  msrrcl  32792  nosgnn0i  33168  sltsolem1  33182  nolt02o  33201  noprc  33251  linedegen  33606  rankeq1o  33634  neufal  33756  neutru  33757  unqsym1  33775  amosym1  33776  onpsstopbas  33780  ordcmp  33797  onint1  33799  bj-ru0  34255  bj-ru  34257  bj-1nel0  34268  bj-0nelsngl  34285  bj-0nmoore  34406  bj-ccinftydisj  34497  bj-isrvec  34577  relowlpssretop  34647  poimirlem16  34910  poimirlem17  34911  poimirlem18  34912  poimirlem19  34913  poimirlem20  34914  poimirlem22  34916  poimirlem30  34924  zrdivrng  35233  prtlem400  36008  equidqe  36060  nsb  39108  eldioph4b  39415  jm2.23  39600  ttac  39640  clsk1indlem1  40402  rusbcALT  40778  fouriersw  42523  aibnbna  43149