Theorem mtand 825

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 416	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 3	mtod 200	1 ⊢ (𝜑 → ¬ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-an 400

This theorem is referenced by:  mteqand  3047  nelpr2  4609  nelpr1  4610  peano5  7868  cofonr  8637  sdomnsym  9067  domnsymfi  9161  unxpdomlem2  9194  cnfcom2lem  9649  cflim2  10213  fin23lem39  10300  isf32lem2  10304  konigthlem  10519  pythagtriplem4  16845  pythagtriplem11  16851  pythagtriplem13  16853  prmreclem1  16942  smndex2dnrinv  18942  psgnunilem5  19524  sylow1lem3  19630  efgredlema  19770  efgredlemc  19775  rrgnz  20740  lssvancl1  20999  lspexchn1  21187  lspindp1  21190  zringlpirlem3  21503  evlslem3  22120  reconnlem2  24875  aaliou2  26391  logdmnrp  26693  dmgmaddnn0  27078  2sqcoprm  27486  pntpbnd1  27637  ostth2lem4  27687  nosepssdm  27737  nolt02olem  27745  nolt02o  27746  nogt01o  27747  nosupbnd1lem3  27761  nosupbnd1lem4  27762  nosupbnd1lem5  27763  nosupbnd1lem6  27764  noinfbnd1lem3  27776  noinfbnd1lem4  27777  noinfbnd1lem5  27778  noinfbnd1lem6  27779  nocvxminlem  27834  sltsdisj  27883  eqcuts3  27884  ltslpss  27988  cofcutr  28004  ltmuls2  28251  bdayfinbndlem1  28547  z12bdaylem1  28550  ncolcom  28717  ncolrot1  28718  ncolrot2  28719  ncoltgdim2  28721  hleqnid  28764  ncolne1  28781  ncolncol  28802  miriso  28826  mirbtwnhl  28836  symquadlem  28845  ragncol  28865  mideulem2  28890  oppne3  28899  opphllem1  28903  opphllem2  28904  opphllem4  28906  opphl  28910  hpgerlem  28921  lmieu  28940  cgrancol  28985  fracfld  33455  rhmpreimaprmidl  33598  qsnzr  33602  prmidlsubm  33606  krullndrng  33629  dflringlem2  33651  dflring3  33653  rsprprmprmidl  33678  esplymhp  33825  0ringirng  33946  constrcon  34031  lmdvg  34210  ballotlemfcc  34751  ballotlemi1  34760  ballotlemii  34761  tgoldbachgtda  34915  morleylemrneab  34925  prv0  35740  ttcwf2  36845  lindsenlbs  38074  mblfinlem1  38116  lcvnbtwn  39609  ncvr1  39856  lnnat  40011  lplncvrlvol  40200  dalem39  40295  lhpocnle  40600  cdleme17b  40871  cdlemg31c  41283  lclkrlem2o  42105  lcfrlem19  42145  baerlem5amN  42300  baerlem5bmN  42301  baerlem5abmN  42302  mapdh8ab  42361  mapdh8ad  42363  mapdh8c  42365  oexpreposd  42891  mullt0b2d  43066  nelsubginvcld  43078  nelsubgcld  43079  fphpd  43353  fiphp3d  43356  pellexlem6  43371  elpell1qr2  43409  pellqrex  43416  pellfund14gap  43424  unxpwdom3  43632  elnelneqd  44738  elnelneq2d  44739  dvgrat  44848  limcperiod  46164  sumnnodd  46166  stirlinglem5  46612  dirkercncflem2  46638  fourierdlem25  46666  fourierdlem63  46703  elaa2  46768  etransclem9  46777  etransclem41  46809  etransclem44  46812  preimagelt  47233  preimalegt  47234  nelsubc2  49650