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 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  3017  nelpr2  4620  nelpr1  4621  peano5  7872  cofonr  8641  sdomnsym  9072  domnsymfi  9170  unxpdomlem2  9205  cnfcom2lem  9661  cflim2  10223  fin23lem39  10310  isf32lem2  10314  konigthlem  10528  pythagtriplem4  16797  pythagtriplem11  16803  pythagtriplem13  16805  prmreclem1  16894  smndex2dnrinv  18849  psgnunilem5  19431  sylow1lem3  19537  efgredlema  19677  efgredlemc  19682  rrgnz  20620  lssvancl1  20858  lspexchn1  21047  lspindp1  21050  zringlpirlem3  21381  evlslem3  21994  reconnlem2  24723  aaliou2  26255  logdmnrp  26557  dmgmaddnn0  26944  2sqcoprm  27353  pntpbnd1  27504  ostth2lem4  27554  nosepssdm  27605  nolt02olem  27613  nolt02o  27614  nogt01o  27615  nosupbnd1lem3  27629  nosupbnd1lem4  27630  nosupbnd1lem5  27631  nosupbnd1lem6  27632  noinfbnd1lem3  27644  noinfbnd1lem4  27645  noinfbnd1lem5  27646  noinfbnd1lem6  27647  nocvxminlem  27696  ssltdisj  27740  sltlpss  27826  cofcutr  27839  sltmul2  28081  ncolcom  28495  ncolrot1  28496  ncolrot2  28497  ncoltgdim2  28499  hleqnid  28542  ncolne1  28559  ncolncol  28580  miriso  28604  mirbtwnhl  28614  symquadlem  28623  ragncol  28643  mideulem2  28668  oppne3  28677  opphllem1  28681  opphllem2  28682  opphllem4  28684  opphl  28688  hpgerlem  28699  lmieu  28718  cgrancol  28763  fracfld  33265  rhmpreimaprmidl  33429  qsnzr  33433  krullndrng  33459  rsprprmprmidl  33500  0ringirng  33691  constrcon  33771  lmdvg  33950  ballotlemfcc  34492  ballotlemi1  34501  ballotlemii  34502  tgoldbachgtda  34659  prv0  35424  lindsenlbs  37616  mblfinlem1  37658  lcvnbtwn  39025  ncvr1  39272  lnnat  39428  lplncvrlvol  39617  dalem39  39712  lhpocnle  40017  cdleme17b  40288  cdlemg31c  40700  lclkrlem2o  41522  lcfrlem19  41562  baerlem5amN  41717  baerlem5bmN  41718  baerlem5abmN  41719  mapdh8ab  41778  mapdh8ad  41780  mapdh8c  41782  oexpreposd  42317  mullt0b2d  42479  nelsubginvcld  42491  nelsubgcld  42492  fphpd  42811  fiphp3d  42814  pellexlem6  42829  elpell1qr2  42867  pellqrex  42874  pellfund14gap  42882  unxpwdom3  43091  elnelneqd  44198  elnelneq2d  44199  dvgrat  44308  limcperiod  45633  sumnnodd  45635  stirlinglem5  46083  dirkercncflem2  46109  fourierdlem25  46137  fourierdlem63  46174  elaa2  46239  etransclem9  46248  etransclem41  46280  etransclem44  46283  preimagelt  46704  preimalegt  46705  nelsubc2  49062