Theorem mtand 828

Description: A modus tollens deduction. (Contributed by Jeff Hankins, 19-Aug-2009.)

Hypotheses

Ref	Expression
mtand.1	⊢ (𝜑 → ¬ 𝜒)
mtand.2	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
mtand	⊢ (𝜑 → ¬ 𝜓)

Proof of Theorem mtand

Step	Hyp	Ref	Expression
1		mtand.1	. 2 ⊢ (𝜑 → ¬ 𝜒)
2		mtand.2	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	2	ex 418	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 3	mtod 201	1 ⊢ (𝜑 → ¬ 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mteqand  3047  elnelneqd  3055  elnelneq2d  3056  nelpr2  4614  nelpr1  4615  peano5  7894  cofonr  8667  sdomnsym  9105  domnsymfi  9199  unxpdomlem2  9232  cnfcom2lem  9686  cflim2  10322  fin23lem39  10409  isf32lem2  10413  konigthlem  10634  pythagtriplem4  16977  pythagtriplem11  16983  pythagtriplem13  16985  prmreclem1  17074  smndex2dnrinv  19094  psgnunilem5  19688  sylow1lem3  19794  efgredlema  19934  efgredlemc  19939  rrgnz  20936  lssvancl1  21200  lspexchn1  21388  lspindp1  21391  rhmpreimaprmidl  21615  qsnzr  21619  prmidlsubm  21623  zringlpirlem3  21750  lindsenlbs  22137  evlslem3  22369  reconnlem2  25127  rnplynfin  26612  plyconz  26613  aaliou2  26649  logdmnrp  26951  dmgmaddnn0  27336  2sqcoprm  27744  pntpbnd1  27895  ostth2lem4  27945  nosepssdm  28025  nolt02olem  28033  nolt02o  28034  nogt01o  28035  nosupbnd1lem3  28049  nosupbnd1lem4  28050  nosupbnd1lem5  28051  nosupbnd1lem6  28052  noinfbnd1lem3  28064  noinfbnd1lem4  28065  noinfbnd1lem5  28066  noinfbnd1lem6  28067  nocvxminlem  28122  sltsdisj  28171  eqcuts3  28172  ltslpss  28276  cofcutr  28292  ltmuls2  28539  bdayfinbndlem1  28835  z12bdaylem1  28838  ncolcom  29006  ncolrot1  29007  ncolrot2  29008  ncoltgdim2  29010  hleqnid  29056  ncolne1  29075  ncolncol  29097  tglnpt4  29105  miriso  29124  mirbtwnhl  29134  symquadlem  29143  symquadprlnglem  29147  ragncol  29166  mideulem2  29192  oppne3  29201  opphllem1  29205  opphllem2  29206  opphllem4  29208  opphl  29212  oppmir  29214  hpgerlem  29225  lnincplng  29244  plngrotlem1  29247  plngrotlem2  29248  lnssplnglem  29251  lnssplng  29252  nhpmirhp  29258  lmieu  29271  cgrancol  29319  tgaaddcpbllem1  29331  tgaaddcpbl  29334  tgaaddcpbl2  29335  angmgmaddeu1  29361  angmgmaddov2lem  29369  dfprlng2  29407  prlngex  29411  prlngmolem1  29412  prlngmolem2  29413  prlnginn0  29420  prlngmid2  29421  prlngsymquadopp  29425  quadcgrprlng  29426  fracfld  33852  krullndrng  33987  dflringlem2  34009  dflring3  34011  rsprprmprmidl  34036  esplymhp  34182  0ringirng  34303  constrcon  34388  lmdvg  34567  ballotlemfcc  35109  ballotlemi1  35118  ballotlemii  35119  tgoldbachgtda  35273  morleylemrneab  35283  prv0  36164  ttcwf2  37283  mblfinlem1  38543  lcvnbtwn  40050  ncvr1  40297  lnnat  40452  lplncvrlvol  40641  dalem39  40736  lhpocnle  41041  cdleme17b  41312  cdlemg31c  41724  lclkrlem2o  42546  lcfrlem19  42586  baerlem5amN  42741  baerlem5bmN  42742  baerlem5abmN  42743  mapdh8ab  42802  mapdh8ad  42804  mapdh8c  42806  oexpreposd  43347  mullt0b2d  43516  nelsubginvcld  43528  nelsubgcld  43529  fphpd  43776  fiphp3d  43779  pellexlem6  43794  elpell1qr2  43832  pellqrex  43839  pellfund14gap  43847  unxpwdom3  44055  dvgrat  45255  limcperiod  46584  sumnnodd  46586  stirlinglem5  47032  dirkercncflem2  47058  fourierdlem25  47086  fourierdlem63  47123  elaa2  47188  etransclem9  47197  etransclem41  47229  etransclem44  47232  preimagelt  47653  preimalegt  47654  nelsubc2  50121