Theorem mtand 828

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mteqand  3048  elnelneqd  3056  elnelneq2d  3057  nelpr2  4617  nelpr1  4618  peano5  7894  cofonr  8666  sdomnsym  9104  domnsymfi  9198  unxpdomlem2  9231  cnfcom2lem  9684  cflim2  10269  fin23lem39  10356  isf32lem2  10360  konigthlem  10581  pythagtriplem4  16917  pythagtriplem11  16923  pythagtriplem13  16925  prmreclem1  17014  smndex2dnrinv  19033  psgnunilem5  19627  sylow1lem3  19733  efgredlema  19873  efgredlemc  19878  rrgnz  20872  lssvancl1  21135  lspexchn1  21323  lspindp1  21326  rhmpreimaprmidl  21548  qsnzr  21552  prmidlsubm  21556  zringlpirlem3  21683  lindsenlbs  22070  evlslem3  22302  reconnlem2  25060  rnplynfin  26546  plyconz  26547  aaliou2  26583  logdmnrp  26886  dmgmaddnn0  27271  2sqcoprm  27679  pntpbnd1  27830  ostth2lem4  27880  nosepssdm  27930  nolt02olem  27938  nolt02o  27939  nogt01o  27940  nosupbnd1lem3  27954  nosupbnd1lem4  27955  nosupbnd1lem5  27956  nosupbnd1lem6  27957  noinfbnd1lem3  27969  noinfbnd1lem4  27970  noinfbnd1lem5  27971  noinfbnd1lem6  27972  nocvxminlem  28027  sltsdisj  28076  eqcuts3  28077  ltslpss  28181  cofcutr  28197  ltmuls2  28444  bdayfinbndlem1  28740  z12bdaylem1  28743  ncolcom  28911  ncolrot1  28912  ncolrot2  28913  ncoltgdim2  28915  hleqnid  28961  ncolne1  28980  ncolncol  29002  tglnpt4  29010  miriso  29029  mirbtwnhl  29039  symquadlem  29048  symquadprlnglem  29052  ragncol  29071  mideulem2  29097  oppne3  29106  opphllem1  29110  opphllem2  29111  opphllem4  29113  opphl  29117  oppmir  29119  hpgerlem  29130  lnincplng  29149  plngrotlem1  29152  plngrotlem2  29153  lnssplnglem  29156  lnssplng  29157  nhpmirhp  29163  lmieu  29176  cgrancol  29224  tgaaddcpbllem1  29236  tgaaddcpbl  29239  tgaaddcpbl2  29240  angmgmaddeu1  29266  angmgmaddov2lem  29274  dfprlng2  29312  prlngex  29316  prlngmolem1  29317  prlngmolem2  29318  prlnginn0  29325  prlngmid2  29326  prlngsymquadopp  29330  quadcgrprlng  29331  fracfld  33757  krullndrng  33891  dflringlem2  33913  dflring3  33915  rsprprmprmidl  33940  esplymhp  34086  0ringirng  34207  constrcon  34292  lmdvg  34471  ballotlemfcc  35013  ballotlemi1  35022  ballotlemii  35023  tgoldbachgtda  35177  morleylemrneab  35187  prv0  36017  ttcwf2  37152  mblfinlem1  38414  lcvnbtwn  39906  ncvr1  40153  lnnat  40308  lplncvrlvol  40497  dalem39  40592  lhpocnle  40897  cdleme17b  41168  cdlemg31c  41580  lclkrlem2o  42402  lcfrlem19  42442  baerlem5amN  42597  baerlem5bmN  42598  baerlem5abmN  42599  mapdh8ab  42658  mapdh8ad  42660  mapdh8c  42662  oexpreposd  43205  mullt0b2d  43380  nelsubginvcld  43392  nelsubgcld  43393  fphpd  43665  fiphp3d  43668  pellexlem6  43683  elpell1qr2  43721  pellqrex  43728  pellfund14gap  43736  unxpwdom3  43944  dvgrat  45144  limcperiod  46466  sumnnodd  46468  stirlinglem5  46914  dirkercncflem2  46940  fourierdlem25  46968  fourierdlem63  47005  elaa2  47070  etransclem9  47079  etransclem41  47111  etransclem44  47114  preimagelt  47535  preimalegt  47536  nelsubc2  50003