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  3050  elnelneqd  3058  elnelneq2d  3059  nelpr2  4614  nelpr1  4615  peano5  7932  cofonr  8714  sdomnsym  9152  domnsymfi  9246  unxpdomlem2  9279  cnfcom2lem  9732  cflim2  10371  fin23lem39  10458  isf32lem2  10462  konigthlem  10683  pythagtriplem4  17029  pythagtriplem11  17035  pythagtriplem13  17037  prmreclem1  17126  smndex2dnrinv  19146  psgnunilem5  19741  sylow1lem3  19847  efgredlema  19987  efgredlemc  19992  rrgnz  20989  lssvancl1  21253  lspexchn1  21441  lspindp1  21444  rhmpreimaprmidl  21668  qsnzr  21672  prmidlsubm  21676  zringlpirlem3  21803  lindsenlbs  22190  evlslem3  22422  reconnlem2  25180  rnplynfin  26663  plyconz  26664  aaliou2  26700  logdmnrp  27002  dmgmaddnn0  27387  2sqcoprm  27795  pntpbnd1  27946  ostth2lem4  27996  nna4b4nsq  28023  nosepssdm  28076  nolt02olem  28084  nolt02o  28085  nogt01o  28086  nosupbnd1lem3  28100  nosupbnd1lem4  28101  nosupbnd1lem5  28102  nosupbnd1lem6  28103  noinfbnd1lem3  28115  noinfbnd1lem4  28116  noinfbnd1lem5  28117  noinfbnd1lem6  28118  nocvxminlem  28173  sltsdisj  28222  eqcuts3  28223  ltslpss  28327  cofcutr  28343  ltmuls2  28590  bdayfinbndlem1  28886  z12bdaylem1  28889  ncolcom  29057  ncolrot1  29058  ncolrot2  29059  ncoltgdim2  29061  hleqnid  29107  ncolne1  29126  ncolncol  29148  tglnpt4  29156  miriso  29175  mirbtwnhl  29185  symquadlem  29194  symquadprlnglem  29198  ragncol  29217  mideulem2  29243  oppne3  29252  opphllem1  29256  opphllem2  29257  opphllem4  29259  opphl  29263  oppmir  29265  hpgerlem  29276  lnincplng  29295  plngrotlem1  29298  plngrotlem2  29299  lnssplnglem  29302  lnssplng  29303  nhpmirhp  29309  lmieu  29322  cgrancol  29370  tgaaddcpbllem1  29382  tgaaddcpbl  29385  tgaaddcpbl2  29386  angmgmaddeu1  29412  angmgmaddov2lem  29420  dfprlng2  29458  prlngex  29462  prlngmolem1  29463  prlngmolem2  29464  prlnginn0  29471  prlngmid2  29472  prlngsymquadopp  29476  quadcgrprlng  29477  tgextamirn  33100  tgextahpl  33102  tgextamirnhl  33105  tgextancgra  33107  tgextalt1  33109  tgextalt2  33110  tgaasncol  33113  fracfld  33954  krullndrng  34089  dflringlem2  34111  dflring3  34113  rsprprmprmidl  34138  esplymhp  34283  0ringirng  34404  constrcon  34489  lmdvg  34668  ballotlemfcc  35209  ballotlemi1  35218  ballotlemii  35219  tgoldbachgtda  35373  morleylemrneab  35383  prv0  36375  ttcwf2  37504  mblfinlem1  38780  lcvnbtwn  40285  ncvr1  40532  lnnat  40687  lplncvrlvol  40876  dalem39  40971  lhpocnle  41276  cdleme17b  41547  cdlemg31c  41959  lclkrlem2o  42781  lcfrlem19  42821  baerlem5amN  42976  baerlem5bmN  42977  baerlem5abmN  42978  mapdh8ab  43037  mapdh8ad  43039  mapdh8c  43041  oexpreposd  43583  mullt0b2d  43752  nelsubginvcld  43764  nelsubgcld  43765  frlmnzcoordex  43856  fphpd  44027  fiphp3d  44030  pellexlem6  44045  elpell1qr2  44083  pellqrex  44090  pellfund14gap  44098  unxpwdom3  44301  dvgrat  45499  limcperiod  46855  sumnnodd  46857  stirlinglem5  47303  dirkercncflem2  47329  fourierdlem25  47357  fourierdlem63  47394  elaa2  47459  etransclem9  47468  etransclem41  47500  etransclem44  47503  preimagelt  47924  preimalegt  47925  nelsubc2  50398