Theorem mtand 815

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

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

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 206  df-an 398

This theorem is referenced by:  mteqand  3034  nelpr2  4656  nelpr1  4657  peano5  7884  peano5OLD  7885  wfrlem16OLD  8324  cofonr  8673  sdomnsym  9098  domnsymfi  9203  unxpdomlem2  9251  cnfcom2lem  9696  cflim2  10258  fin23lem39  10345  isf32lem2  10349  konigthlem  10563  pythagtriplem4  16752  pythagtriplem11  16758  pythagtriplem13  16760  prmreclem1  16849  smndex2dnrinv  18796  psgnunilem5  19362  sylow1lem3  19468  efgredlema  19608  efgredlemc  19613  lssvancl1  20555  lspexchn1  20743  lspindp1  20746  zringlpirlem3  21034  evlslem3  21643  reconnlem2  24343  aaliou2  25853  logdmnrp  26149  dmgmaddnn0  26531  2sqcoprm  26938  pntpbnd1  27089  ostth2lem4  27139  nosepssdm  27189  nolt02olem  27197  nolt02o  27198  nogt01o  27199  nosupbnd1lem3  27213  nosupbnd1lem4  27214  nosupbnd1lem5  27215  nosupbnd1lem6  27216  noinfbnd1lem3  27228  noinfbnd1lem4  27229  noinfbnd1lem5  27230  noinfbnd1lem6  27231  nocvxminlem  27279  ssltdisj  27322  sltlpss  27401  cofcutr  27411  sltmul2  27623  ncolcom  27812  ncolrot1  27813  ncolrot2  27814  ncoltgdim2  27816  hleqnid  27859  ncolne1  27876  ncolncol  27897  miriso  27921  mirbtwnhl  27931  symquadlem  27940  ragncol  27960  mideulem2  27985  oppne3  27994  opphllem1  27998  opphllem2  27999  opphllem4  28001  opphl  28005  hpgerlem  28016  lmieu  28035  cgrancol  28080  rhmpreimaprmidl  32570  qsnzr  32574  0ringirng  32753  lmdvg  32933  ballotlemfcc  33492  ballotlemi1  33501  ballotlemii  33502  tgoldbachgtda  33673  prv0  34421  lindsenlbs  36483  mblfinlem1  36525  lcvnbtwn  37895  ncvr1  38142  lnnat  38298  lplncvrlvol  38487  dalem39  38582  lhpocnle  38887  cdleme17b  39158  cdlemg31c  39570  lclkrlem2o  40392  lcfrlem19  40432  baerlem5amN  40587  baerlem5bmN  40588  baerlem5abmN  40589  mapdh8ab  40648  mapdh8ad  40650  mapdh8c  40652  nelsubginvcld  41070  nelsubgcld  41071  oexpreposd  41212  fphpd  41554  fiphp3d  41557  pellexlem6  41572  elpell1qr2  41610  pellqrex  41617  pellfund14gap  41625  unxpwdom3  41837  elnelneqd  42954  elnelneq2d  42955  dvgrat  43071  limcperiod  44344  sumnnodd  44346  stirlinglem5  44794  dirkercncflem2  44820  fourierdlem25  44848  fourierdlem63  44885  elaa2  44950  etransclem9  44959  etransclem41  44991  etransclem44  44994  preimagelt  45415  preimalegt  45416