Theorem mtand 816

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

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

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 207  df-an 396

This theorem is referenced by:  mteqand  3023  nelpr2  4597  nelpr1  4598  peano5  7844  cofonr  8610  sdomnsym  9040  domnsymfi  9134  unxpdomlem2  9167  cnfcom2lem  9622  cflim2  10185  fin23lem39  10272  isf32lem2  10276  konigthlem  10491  pythagtriplem4  16790  pythagtriplem11  16796  pythagtriplem13  16798  prmreclem1  16887  smndex2dnrinv  18886  psgnunilem5  19469  sylow1lem3  19575  efgredlema  19715  efgredlemc  19720  rrgnz  20681  lssvancl1  20940  lspexchn1  21128  lspindp1  21131  zringlpirlem3  21444  evlslem3  22058  reconnlem2  24793  aaliou2  26306  logdmnrp  26605  dmgmaddnn0  26990  2sqcoprm  27398  pntpbnd1  27549  ostth2lem4  27599  nosepssdm  27650  nolt02olem  27658  nolt02o  27659  nogt01o  27660  nosupbnd1lem3  27674  nosupbnd1lem4  27675  nosupbnd1lem5  27676  nosupbnd1lem6  27677  noinfbnd1lem3  27689  noinfbnd1lem4  27690  noinfbnd1lem5  27691  noinfbnd1lem6  27692  nocvxminlem  27746  sltsdisj  27795  eqcuts3  27796  ltslpss  27900  cofcutr  27916  ltmuls2  28163  bdayfinbndlem1  28459  z12bdaylem1  28462  ncolcom  28629  ncolrot1  28630  ncolrot2  28631  ncoltgdim2  28633  hleqnid  28676  ncolne1  28693  ncolncol  28714  miriso  28738  mirbtwnhl  28748  symquadlem  28757  ragncol  28777  mideulem2  28802  oppne3  28811  opphllem1  28815  opphllem2  28816  opphllem4  28818  opphl  28822  hpgerlem  28833  lmieu  28852  cgrancol  28897  fracfld  33369  rhmpreimaprmidl  33511  qsnzr  33515  krullndrng  33541  rsprprmprmidl  33582  esplymhp  33712  0ringirng  33833  constrcon  33918  lmdvg  34097  ballotlemfcc  34638  ballotlemi1  34647  ballotlemii  34648  tgoldbachgtda  34805  prv0  35612  ttcwf2  36707  lindsenlbs  37936  mblfinlem1  37978  lcvnbtwn  39471  ncvr1  39718  lnnat  39873  lplncvrlvol  40062  dalem39  40157  lhpocnle  40462  cdleme17b  40733  cdlemg31c  41145  lclkrlem2o  41967  lcfrlem19  42007  baerlem5amN  42162  baerlem5bmN  42163  baerlem5abmN  42164  mapdh8ab  42223  mapdh8ad  42225  mapdh8c  42227  oexpreposd  42754  mullt0b2d  42929  nelsubginvcld  42941  nelsubgcld  42942  fphpd  43244  fiphp3d  43247  pellexlem6  43262  elpell1qr2  43300  pellqrex  43307  pellfund14gap  43315  unxpwdom3  43523  elnelneqd  44629  elnelneq2d  44630  dvgrat  44739  limcperiod  46058  sumnnodd  46060  stirlinglem5  46506  dirkercncflem2  46532  fourierdlem25  46560  fourierdlem63  46597  elaa2  46662  etransclem9  46671  etransclem41  46703  etransclem44  46706  preimagelt  47127  preimalegt  47128  nelsubc2  49544