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

Theorem mtand 691
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 450 . 2 (𝜑 → (𝜓𝜒))
41, 3mtod 189 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384
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 197  df-an 386
This theorem is referenced by:  peano5  7086  wfrlem16  7427  sdomnsym  8082  unxpdomlem2  8162  cnfcom2lem  8595  cflim2  9082  fin23lem39  9169  isf32lem2  9173  konigthlem  9387  pythagtriplem4  15518  pythagtriplem11  15524  pythagtriplem13  15526  prmreclem1  15614  psgnunilem5  17908  sylow1lem3  18009  efgredlema  18147  efgredlemc  18152  lssvancl1  18939  lspexchn1  19124  lspindp1  19127  evlslem3  19508  zringlpirlem3  19828  reconnlem2  22624  aaliou2  24089  logdmnrp  24381  dmgmaddnn0  24747  pntpbnd1  25269  ostth2lem4  25319  ncolcom  25450  ncolrot1  25451  ncolrot2  25452  ncoltgdim2  25454  hleqnid  25497  ncolne1  25514  ncolncol  25535  miriso  25559  mirbtwnhl  25569  symquadlem  25578  ragncol  25598  mideulem2  25620  opphllem2  25634  opphllem4  25636  opphl  25640  hpgerlem  25651  lmieu  25670  2sqcoprm  29632  lmdvg  29984  ballotlemfcc  30540  ballotlemi1  30549  ballotlemii  30550  tgoldbachgtda  30724  nosepssdm  31820  nolt02olem  31828  nolt02o  31829  nosupbnd1lem3  31840  nosupbnd1lem4  31841  nosupbnd1lem5  31842  nosupbnd1lem6  31843  nocvxminlem  31877  lindsenlbs  33384  mblfinlem1  33426  lcvnbtwn  34138  ncvr1  34385  lnnat  34539  lplncvrlvol  34728  dalem39  34823  lhpocnle  35128  cdleme17b  35400  cdlemg31c  35813  lclkrlem2o  36636  lcfrlem19  36676  baerlem5amN  36831  baerlem5bmN  36832  baerlem5abmN  36833  mapdh8ab  36892  mapdh8ad  36894  mapdh8c  36896  fphpd  37206  fiphp3d  37209  pellexlem6  37224  elpell1qr2  37262  pellqrex  37269  pellfund14gap  37277  unxpwdom3  37491  dvgrat  38337  nelpr2  39087  nelpr1  39088  limcperiod  39666  sumnnodd  39668  stirlinglem5  40064  dirkercncflem2  40090  fourierdlem25  40118  fourierdlem63  40155  elaa2  40220  etransclem9  40229  etransclem41  40261  etransclem44  40264
  Copyright terms: Public domain W3C validator