MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mtand Structured version   Visualization version   GIF version

Theorem mtand 812
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
StepHypRef Expression
1 mtand.1 . 2 (𝜑 → ¬ 𝜒)
2 mtand.2 . . 3 ((𝜑𝜓) → 𝜒)
32ex 413 . 2 (𝜑 → (𝜓𝜒))
41, 3mtod 199 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
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 208  df-an 397
This theorem is referenced by:  mteqand  3122  nelpr2  4584  nelpr1  4585  peano5  7593  wfrlem16  7961  sdomnsym  8631  unxpdomlem2  8712  cnfcom2lem  9153  cflim2  9674  fin23lem39  9761  isf32lem2  9765  konigthlem  9979  pythagtriplem4  16146  pythagtriplem11  16152  pythagtriplem13  16154  prmreclem1  16242  psgnunilem5  18553  sylow1lem3  18656  efgredlema  18797  efgredlemc  18802  lssvancl1  19647  lspexchn1  19833  lspindp1  19836  evlslem3  20223  zringlpirlem3  20563  reconnlem2  23364  aaliou2  24858  logdmnrp  25151  dmgmaddnn0  25532  2sqcoprm  25939  pntpbnd1  26090  ostth2lem4  26140  ncolcom  26275  ncolrot1  26276  ncolrot2  26277  ncoltgdim2  26279  hleqnid  26322  ncolne1  26339  ncolncol  26360  miriso  26384  mirbtwnhl  26394  symquadlem  26403  ragncol  26423  mideulem2  26448  oppne3  26457  opphllem1  26461  opphllem2  26462  opphllem4  26464  opphl  26468  hpgerlem  26479  lmieu  26498  cgrancol  26543  lmdvg  31096  ballotlemfcc  31651  ballotlemi1  31660  ballotlemii  31661  tgoldbachgtda  31832  prv0  32575  nosepssdm  33088  nolt02olem  33096  nolt02o  33097  nosupbnd1lem3  33108  nosupbnd1lem4  33109  nosupbnd1lem5  33110  nosupbnd1lem6  33111  nocvxminlem  33145  lindsenlbs  34769  mblfinlem1  34811  lcvnbtwn  36043  ncvr1  36290  lnnat  36445  lplncvrlvol  36634  dalem39  36729  lhpocnle  37034  cdleme17b  37305  cdlemg31c  37717  lclkrlem2o  38539  lcfrlem19  38579  baerlem5amN  38734  baerlem5bmN  38735  baerlem5abmN  38736  mapdh8ab  38795  mapdh8ad  38797  mapdh8c  38799  nelsubginvcld  39008  nelsubgcld  39009  oexpreposd  39059  fphpd  39293  fiphp3d  39296  pellexlem6  39311  elpell1qr2  39349  pellqrex  39356  pellfund14gap  39364  unxpwdom3  39575  elnelneqd  40436  elnelneq2d  40437  dvgrat  40524  limcperiod  41789  sumnnodd  41791  stirlinglem5  42244  dirkercncflem2  42270  fourierdlem25  42298  fourierdlem63  42335  elaa2  42400  etransclem9  42409  etransclem41  42441  etransclem44  42444  preimagelt  42861  preimalegt  42862  smndex2dnrinv  43985
  Copyright terms: Public domain W3C validator