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

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
StepHypRef Expression
1 mtand.1 . 2 (𝜑 → ¬ 𝜒)
2 mtand.2 . . 3 ((𝜑𝜓) → 𝜒)
32ex 416 . 2 (𝜑 → (𝜓𝜒))
41, 3mtod 201 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  mteqand  3093  nelpr2  4555  nelpr1  4556  peano5  7589  wfrlem16  7957  sdomnsym  8630  unxpdomlem2  8711  cnfcom2lem  9152  cflim2  9678  fin23lem39  9765  isf32lem2  9769  konigthlem  9983  pythagtriplem4  16149  pythagtriplem11  16155  pythagtriplem13  16157  prmreclem1  16245  smndex2dnrinv  18075  psgnunilem5  18617  sylow1lem3  18720  efgredlema  18861  efgredlemc  18866  lssvancl1  19712  lspexchn1  19898  lspindp1  19901  zringlpirlem3  20182  evlslem3  20755  reconnlem2  23435  aaliou2  24939  logdmnrp  25235  dmgmaddnn0  25615  2sqcoprm  26022  pntpbnd1  26173  ostth2lem4  26223  ncolcom  26358  ncolrot1  26359  ncolrot2  26360  ncoltgdim2  26362  hleqnid  26405  ncolne1  26422  ncolncol  26443  miriso  26467  mirbtwnhl  26477  symquadlem  26486  ragncol  26506  mideulem2  26531  oppne3  26540  opphllem1  26544  opphllem2  26545  opphllem4  26547  opphl  26551  hpgerlem  26562  lmieu  26581  cgrancol  26626  rhmpreimaprmidl  31035  lmdvg  31304  ballotlemfcc  31859  ballotlemi1  31868  ballotlemii  31869  tgoldbachgtda  32040  prv0  32785  nosepssdm  33298  nolt02olem  33306  nolt02o  33307  nosupbnd1lem3  33318  nosupbnd1lem4  33319  nosupbnd1lem5  33320  nosupbnd1lem6  33321  nocvxminlem  33355  lindsenlbs  35045  mblfinlem1  35087  lcvnbtwn  36314  ncvr1  36561  lnnat  36716  lplncvrlvol  36905  dalem39  37000  lhpocnle  37305  cdleme17b  37576  cdlemg31c  37988  lclkrlem2o  38810  lcfrlem19  38850  baerlem5amN  39005  baerlem5bmN  39006  baerlem5abmN  39007  mapdh8ab  39066  mapdh8ad  39068  mapdh8c  39070  nelsubginvcld  39410  nelsubgcld  39411  oexpreposd  39474  fphpd  39744  fiphp3d  39747  pellexlem6  39762  elpell1qr2  39800  pellqrex  39807  pellfund14gap  39815  unxpwdom3  40026  elnelneqd  40895  elnelneq2d  40896  dvgrat  41003  limcperiod  42257  sumnnodd  42259  stirlinglem5  42707  dirkercncflem2  42733  fourierdlem25  42761  fourierdlem63  42798  elaa2  42863  etransclem9  42872  etransclem41  42904  etransclem44  42907  preimagelt  43324  preimalegt  43325
  Copyright terms: Public domain W3C validator