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  3033  nelpr2  4653  nelpr1  4654  peano5  7915  wfrlem16OLD  8364  cofonr  8712  sdomnsym  9138  domnsymfi  9240  unxpdomlem2  9287  cnfcom2lem  9741  cflim2  10303  fin23lem39  10390  isf32lem2  10394  konigthlem  10608  pythagtriplem4  16857  pythagtriplem11  16863  pythagtriplem13  16865  prmreclem1  16954  smndex2dnrinv  18928  psgnunilem5  19512  sylow1lem3  19618  efgredlema  19758  efgredlemc  19763  rrgnz  20704  lssvancl1  20943  lspexchn1  21132  lspindp1  21135  zringlpirlem3  21475  evlslem3  22104  reconnlem2  24849  aaliou2  26382  logdmnrp  26683  dmgmaddnn0  27070  2sqcoprm  27479  pntpbnd1  27630  ostth2lem4  27680  nosepssdm  27731  nolt02olem  27739  nolt02o  27740  nogt01o  27741  nosupbnd1lem3  27755  nosupbnd1lem4  27756  nosupbnd1lem5  27757  nosupbnd1lem6  27758  noinfbnd1lem3  27770  noinfbnd1lem4  27771  noinfbnd1lem5  27772  noinfbnd1lem6  27773  nocvxminlem  27822  ssltdisj  27866  sltlpss  27945  cofcutr  27958  sltmul2  28197  ncolcom  28569  ncolrot1  28570  ncolrot2  28571  ncoltgdim2  28573  hleqnid  28616  ncolne1  28633  ncolncol  28654  miriso  28678  mirbtwnhl  28688  symquadlem  28697  ragncol  28717  mideulem2  28742  oppne3  28751  opphllem1  28755  opphllem2  28756  opphllem4  28758  opphl  28762  hpgerlem  28773  lmieu  28792  cgrancol  28837  fracfld  33310  rhmpreimaprmidl  33479  qsnzr  33483  krullndrng  33509  rsprprmprmidl  33550  0ringirng  33739  lmdvg  33952  ballotlemfcc  34496  ballotlemi1  34505  ballotlemii  34506  tgoldbachgtda  34676  prv0  35435  lindsenlbs  37622  mblfinlem1  37664  lcvnbtwn  39026  ncvr1  39273  lnnat  39429  lplncvrlvol  39618  dalem39  39713  lhpocnle  40018  cdleme17b  40289  cdlemg31c  40701  lclkrlem2o  41523  lcfrlem19  41563  baerlem5amN  41718  baerlem5bmN  41719  baerlem5abmN  41720  mapdh8ab  41779  mapdh8ad  41781  mapdh8c  41783  oexpreposd  42357  nelsubginvcld  42506  nelsubgcld  42507  fphpd  42827  fiphp3d  42830  pellexlem6  42845  elpell1qr2  42883  pellqrex  42890  pellfund14gap  42898  unxpwdom3  43107  elnelneqd  44215  elnelneq2d  44216  dvgrat  44331  limcperiod  45643  sumnnodd  45645  stirlinglem5  46093  dirkercncflem2  46119  fourierdlem25  46147  fourierdlem63  46184  elaa2  46249  etransclem9  46258  etransclem41  46290  etransclem44  46293  preimagelt  46714  preimalegt  46715