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

Theorem mt3d 132
Description: Modus tollens deduction. (Contributed by NM, 26-Mar-1995.)
Hypotheses
Ref Expression
mt3d.1 (𝜑 → ¬ 𝜒)
mt3d.2 (𝜑 → (¬ 𝜓𝜒))
Assertion
Ref Expression
mt3d (𝜑𝜓)

Proof of Theorem mt3d
StepHypRef Expression
1 mt3d.1 . 2 (𝜑 → ¬ 𝜒)
2 mt3d.2 . . 3 (𝜑 → (¬ 𝜓𝜒))
32con1d 131 . 2 (𝜑 → (¬ 𝜒𝜓))
41, 3mpd 15 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  mt3i  133  nsyl2  134  ecase23d  1417  disjss3  4433  nnsuc  6786  unxpdomlem2  7861  oismo  8138  cnfcom3lem  8293  rankelb  8380  fin33i  8884  isf34lem4  8892  canthp1lem2  9163  gchcda1  9166  pwfseqlem3  9170  inttsk  9284  r1tskina  9292  nqereu  9439  zbtwnre  11353  discr1  12522  seqcoll2  12751  dvdseq  14512  bitsfzo  14571  bitsf1  14582  eucalglt  14706  4sqlem17OLD  15067  4sqlem18OLD  15068  4sqlem17  15073  4sqlem18  15074  ramubcl  15138  psgnunilem5  17296  odnncl  17355  gexnnod  17401  sylow1lem1  17411  torsubg  17653  prmcyg  17689  ablfacrplem  17858  pgpfac1lem2  17868  pgpfac1lem3a  17869  pgpfac1lem3  17870  xrsdsreclblem  19172  prmirredlem  19222  ppttop  20179  pptbas  20180  regr1lem  20911  alexsublem  21217  reconnlem1  22002  metnrmlem1a  22033  metnrmlem1aOLD  22048  vitalilem4  22730  vitalilem5  22731  itg2gt0  22879  rollelem  23102  lhop1lem  23126  coefv0  23363  plyexmo  23427  lgamucov  24124  ppinprm  24240  chtnprm  24242  lgsdir  24419  lgseisenlem1  24438  2sqlem7  24459  2sqblem  24466  pntpbnd1  24585  dfon2lem8  30587  nobndup  30740  nobnddown  30741  nofulllem5  30746  poimirlem25  32203  fdc  32311  ac6s6  32651  2atm  33332  llnmlplnN  33344  trlval3  33993  cdleme0moN  34031  cdleme18c  34099  qirropth  35996  aacllem  41727
  Copyright terms: Public domain W3C validator