Theorem mtand 813

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

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

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 397

This theorem is referenced by:  mteqand  3046  nelpr2  4596  nelpr1  4597  peano5  7783  peano5OLD  7784  wfrlem16OLD  8200  sdomnsym  8938  domnsymfi  9043  unxpdomlem2  9091  cnfcom2lem  9527  cflim2  10089  fin23lem39  10176  isf32lem2  10180  konigthlem  10394  pythagtriplem4  16587  pythagtriplem11  16593  pythagtriplem13  16595  prmreclem1  16684  smndex2dnrinv  18621  psgnunilem5  19169  sylow1lem3  19272  efgredlema  19413  efgredlemc  19418  lssvancl1  20277  lspexchn1  20463  lspindp1  20466  zringlpirlem3  20757  evlslem3  21361  reconnlem2  24061  aaliou2  25571  logdmnrp  25867  dmgmaddnn0  26247  2sqcoprm  26654  pntpbnd1  26805  ostth2lem4  26855  ncolcom  27030  ncolrot1  27031  ncolrot2  27032  ncoltgdim2  27034  hleqnid  27077  ncolne1  27094  ncolncol  27115  miriso  27139  mirbtwnhl  27149  symquadlem  27158  ragncol  27178  mideulem2  27203  oppne3  27212  opphllem1  27216  opphllem2  27217  opphllem4  27219  opphl  27223  hpgerlem  27234  lmieu  27253  cgrancol  27298  rhmpreimaprmidl  31732  lmdvg  32009  ballotlemfcc  32566  ballotlemi1  32575  ballotlemii  32576  tgoldbachgtda  32747  prv0  33498  nosepssdm  33950  nolt02olem  33958  nolt02o  33959  nogt01o  33960  nosupbnd1lem3  33974  nosupbnd1lem4  33975  nosupbnd1lem5  33976  nosupbnd1lem6  33977  noinfbnd1lem3  33989  noinfbnd1lem4  33990  noinfbnd1lem5  33991  noinfbnd1lem6  33992  nocvxminlem  34033  ssltdisj  34076  sltlpss  34148  cofcutr  34153  lindsenlbs  35832  mblfinlem1  35874  lcvnbtwn  37251  ncvr1  37498  lnnat  37653  lplncvrlvol  37842  dalem39  37937  lhpocnle  38242  cdleme17b  38513  cdlemg31c  38925  lclkrlem2o  39747  lcfrlem19  39787  baerlem5amN  39942  baerlem5bmN  39943  baerlem5abmN  39944  mapdh8ab  40003  mapdh8ad  40005  mapdh8c  40007  nelsubginvcld  40430  nelsubgcld  40431  oexpreposd  40531  fphpd  40848  fiphp3d  40851  pellexlem6  40866  elpell1qr2  40904  pellqrex  40911  pellfund14gap  40919  unxpwdom3  41131  elnelneqd  42041  elnelneq2d  42042  dvgrat  42158  limcperiod  43413  sumnnodd  43415  stirlinglem5  43863  dirkercncflem2  43889  fourierdlem25  43917  fourierdlem63  43954  elaa2  44019  etransclem9  44028  etransclem41  44060  etransclem44  44063  preimagelt  44482  preimalegt  44483