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  3049  nelpr2  4589  nelpr1  4590  peano5  7749  peano5OLD  7750  wfrlem16OLD  8164  sdomnsym  8894  domnsymfi  8995  unxpdomlem2  9037  cnfcom2lem  9468  cflim2  10028  fin23lem39  10115  isf32lem2  10119  konigthlem  10333  pythagtriplem4  16529  pythagtriplem11  16535  pythagtriplem13  16537  prmreclem1  16626  smndex2dnrinv  18563  psgnunilem5  19111  sylow1lem3  19214  efgredlema  19355  efgredlemc  19360  lssvancl1  20215  lspexchn1  20401  lspindp1  20404  zringlpirlem3  20695  evlslem3  21299  reconnlem2  23999  aaliou2  25509  logdmnrp  25805  dmgmaddnn0  26185  2sqcoprm  26592  pntpbnd1  26743  ostth2lem4  26793  ncolcom  26931  ncolrot1  26932  ncolrot2  26933  ncoltgdim2  26935  hleqnid  26978  ncolne1  26995  ncolncol  27016  miriso  27040  mirbtwnhl  27050  symquadlem  27059  ragncol  27079  mideulem2  27104  oppne3  27113  opphllem1  27117  opphllem2  27118  opphllem4  27120  opphl  27124  hpgerlem  27135  lmieu  27154  cgrancol  27199  rhmpreimaprmidl  31636  lmdvg  31912  ballotlemfcc  32469  ballotlemi1  32478  ballotlemii  32479  tgoldbachgtda  32650  prv0  33401  nosepssdm  33898  nolt02olem  33906  nolt02o  33907  nogt01o  33908  nosupbnd1lem3  33922  nosupbnd1lem4  33923  nosupbnd1lem5  33924  nosupbnd1lem6  33925  noinfbnd1lem3  33937  noinfbnd1lem4  33938  noinfbnd1lem5  33939  noinfbnd1lem6  33940  nocvxminlem  33981  ssltdisj  34024  sltlpss  34096  cofcutr  34101  lindsenlbs  35781  mblfinlem1  35823  lcvnbtwn  37046  ncvr1  37293  lnnat  37448  lplncvrlvol  37637  dalem39  37732  lhpocnle  38037  cdleme17b  38308  cdlemg31c  38720  lclkrlem2o  39542  lcfrlem19  39582  baerlem5amN  39737  baerlem5bmN  39738  baerlem5abmN  39739  mapdh8ab  39798  mapdh8ad  39800  mapdh8c  39802  nelsubginvcld  40227  nelsubgcld  40228  oexpreposd  40328  fphpd  40645  fiphp3d  40648  pellexlem6  40663  elpell1qr2  40701  pellqrex  40708  pellfund14gap  40716  unxpwdom3  40927  elnelneqd  41820  elnelneq2d  41821  dvgrat  41937  limcperiod  43176  sumnnodd  43178  stirlinglem5  43626  dirkercncflem2  43652  fourierdlem25  43680  fourierdlem63  43717  elaa2  43782  etransclem9  43791  etransclem41  43823  etransclem44  43826  preimagelt  44244  preimalegt  44245