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  4655  nelpr1  4656  peano5  7881  peano5OLD  7882  wfrlem16OLD  8321  cofonr  8670  sdomnsym  9095  domnsymfi  9200  unxpdomlem2  9248  cnfcom2lem  9693  cflim2  10255  fin23lem39  10342  isf32lem2  10346  konigthlem  10560  pythagtriplem4  16749  pythagtriplem11  16755  pythagtriplem13  16757  prmreclem1  16846  smndex2dnrinv  18793  psgnunilem5  19357  sylow1lem3  19463  efgredlema  19603  efgredlemc  19608  lssvancl1  20548  lspexchn1  20736  lspindp1  20739  zringlpirlem3  21026  evlslem3  21635  reconnlem2  24335  aaliou2  25845  logdmnrp  26141  dmgmaddnn0  26521  2sqcoprm  26928  pntpbnd1  27079  ostth2lem4  27129  nosepssdm  27179  nolt02olem  27187  nolt02o  27188  nogt01o  27189  nosupbnd1lem3  27203  nosupbnd1lem4  27204  nosupbnd1lem5  27205  nosupbnd1lem6  27206  noinfbnd1lem3  27218  noinfbnd1lem4  27219  noinfbnd1lem5  27220  noinfbnd1lem6  27221  nocvxminlem  27269  ssltdisj  27312  sltlpss  27391  cofcutr  27401  sltmul2  27613  ncolcom  27802  ncolrot1  27803  ncolrot2  27804  ncoltgdim2  27806  hleqnid  27849  ncolne1  27866  ncolncol  27887  miriso  27911  mirbtwnhl  27921  symquadlem  27930  ragncol  27950  mideulem2  27975  oppne3  27984  opphllem1  27988  opphllem2  27989  opphllem4  27991  opphl  27995  hpgerlem  28006  lmieu  28025  cgrancol  28070  rhmpreimaprmidl  32559  qsnzr  32563  0ringirng  32742  lmdvg  32922  ballotlemfcc  33481  ballotlemi1  33490  ballotlemii  33491  tgoldbachgtda  33662  prv0  34410  lindsenlbs  36472  mblfinlem1  36514  lcvnbtwn  37884  ncvr1  38131  lnnat  38287  lplncvrlvol  38476  dalem39  38571  lhpocnle  38876  cdleme17b  39147  cdlemg31c  39559  lclkrlem2o  40381  lcfrlem19  40421  baerlem5amN  40576  baerlem5bmN  40577  baerlem5abmN  40578  mapdh8ab  40637  mapdh8ad  40639  mapdh8c  40641  nelsubginvcld  41068  nelsubgcld  41069  oexpreposd  41208  fphpd  41540  fiphp3d  41543  pellexlem6  41558  elpell1qr2  41596  pellqrex  41603  pellfund14gap  41611  unxpwdom3  41823  elnelneqd  42940  elnelneq2d  42941  dvgrat  43057  limcperiod  44331  sumnnodd  44333  stirlinglem5  44781  dirkercncflem2  44807  fourierdlem25  44835  fourierdlem63  44872  elaa2  44937  etransclem9  44946  etransclem41  44978  etransclem44  44981  preimagelt  45402  preimalegt  45403