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  3046  elnelneqd  3054  elnelneq2d  3055  nelpr2  4610  nelpr1  4611  peano5  7906  cofonr  8687  sdomnsym  9125  domnsymfi  9219  unxpdomlem2  9252  cnfcom2lem  9706  cflim2  10345  fin23lem39  10432  isf32lem2  10436  konigthlem  10657  pythagtriplem4  17003  pythagtriplem11  17009  pythagtriplem13  17011  prmreclem1  17100  smndex2dnrinv  19120  psgnunilem5  19714  sylow1lem3  19820  efgredlema  19960  efgredlemc  19965  rrgnz  20962  lssvancl1  21226  lspexchn1  21414  lspindp1  21417  rhmpreimaprmidl  21641  qsnzr  21645  prmidlsubm  21649  zringlpirlem3  21776  lindsenlbs  22163  evlslem3  22395  reconnlem2  25153  rnplynfin  26636  plyconz  26637  aaliou2  26673  logdmnrp  26975  dmgmaddnn0  27360  2sqcoprm  27768  pntpbnd1  27919  ostth2lem4  27969  nna4b4nsq  27996  nosepssdm  28049  nolt02olem  28057  nolt02o  28058  nogt01o  28059  nosupbnd1lem3  28073  nosupbnd1lem4  28074  nosupbnd1lem5  28075  nosupbnd1lem6  28076  noinfbnd1lem3  28088  noinfbnd1lem4  28089  noinfbnd1lem5  28090  noinfbnd1lem6  28091  nocvxminlem  28146  sltsdisj  28195  eqcuts3  28196  ltslpss  28300  cofcutr  28316  ltmuls2  28563  bdayfinbndlem1  28859  z12bdaylem1  28862  ncolcom  29030  ncolrot1  29031  ncolrot2  29032  ncoltgdim2  29034  hleqnid  29080  ncolne1  29099  ncolncol  29121  tglnpt4  29129  miriso  29148  mirbtwnhl  29158  symquadlem  29167  symquadprlnglem  29171  ragncol  29190  mideulem2  29216  oppne3  29225  opphllem1  29229  opphllem2  29230  opphllem4  29232  opphl  29236  oppmir  29238  hpgerlem  29249  lnincplng  29268  plngrotlem1  29271  plngrotlem2  29272  lnssplnglem  29275  lnssplng  29276  nhpmirhp  29282  lmieu  29295  cgrancol  29343  tgaaddcpbllem1  29355  tgaaddcpbl  29358  tgaaddcpbl2  29359  angmgmaddeu1  29385  angmgmaddov2lem  29393  dfprlng2  29431  prlngex  29435  prlngmolem1  29436  prlngmolem2  29437  prlnginn0  29444  prlngmid2  29445  prlngsymquadopp  29449  quadcgrprlng  29450  tgextamirn  33073  tgextahpl  33075  tgextamirnhl  33078  tgextancgra  33080  tgextalt1  33082  tgextalt2  33083  tgaasncol  33086  fracfld  33917  krullndrng  34052  dflringlem2  34074  dflring3  34076  rsprprmprmidl  34101  esplymhp  34247  0ringirng  34368  constrcon  34453  lmdvg  34632  ballotlemfcc  35173  ballotlemi1  35182  ballotlemii  35183  tgoldbachgtda  35337  morleylemrneab  35347  prv0  36282  ttcwf2  37406  mblfinlem1  38669  lcvnbtwn  40176  ncvr1  40423  lnnat  40578  lplncvrlvol  40767  dalem39  40862  lhpocnle  41167  cdleme17b  41438  cdlemg31c  41850  lclkrlem2o  42672  lcfrlem19  42712  baerlem5amN  42867  baerlem5bmN  42868  baerlem5abmN  42869  mapdh8ab  42928  mapdh8ad  42930  mapdh8c  42932  oexpreposd  43473  mullt0b2d  43642  nelsubginvcld  43654  nelsubgcld  43655  frlmnzcoordex  43746  fphpd  43917  fiphp3d  43920  pellexlem6  43935  elpell1qr2  43973  pellqrex  43980  pellfund14gap  43988  unxpwdom3  44191  dvgrat  45390  limcperiod  46734  sumnnodd  46736  stirlinglem5  47182  dirkercncflem2  47208  fourierdlem25  47236  fourierdlem63  47273  elaa2  47338  etransclem9  47347  etransclem41  47379  etransclem44  47382  preimagelt  47803  preimalegt  47804  nelsubc2  50277