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

Theorem mt2d 134
Description: Modus tollens deduction. (Contributed by NM, 4-Jul-1994.)
Hypotheses
Ref Expression
mt2d.1 (𝜑𝜒)
mt2d.2 (𝜑 → (𝜓 → ¬ 𝜒))
Assertion
Ref Expression
mt2d (𝜑 → ¬ 𝜓)

Proof of Theorem mt2d
StepHypRef Expression
1 mt2d.1 . 2 (𝜑𝜒)
2 mt2d.2 . . 3 (𝜑 → (𝜓 → ¬ 𝜒))
32con2d 132 . 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:  mt2i  135  nsyl3  136  tz7.44-3  7775  sdomdomtr  8368  domsdomtr  8370  infdif  9353  ackbij1b  9383  isf32lem5  9501  alephreg  9726  cfpwsdom  9728  inar1  9919  tskcard  9925  npomex  10140  recnz  11787  rpnnen1lem5  12110  fznuz  12723  uznfz  12724  seqcoll2  13545  ramub1lem1  16108  pgpfac1lem1  18834  lsppratlem6  19520  nconnsubb  21604  iunconnlem  21608  clsconn  21611  xkohaus  21834  reconnlem1  23006  ivthlem2  23625  perfectlem1  25374  lgseisenlem1  25520  ex-natded5.8-2  27825  oddpwdc  30957  erdszelem9  31723  relowlpssretop  33752  sucneqond  33753  heiborlem8  34154  lcvntr  35096  ncvr1  35342  llnneat  35584  2atnelpln  35614  lplnneat  35615  lplnnelln  35616  3atnelvolN  35656  lvolneatN  35658  lvolnelln  35659  lvolnelpln  35660  lplncvrlvol  35686  4atexlemntlpq  36138  cdleme0nex  36360
  Copyright terms: Public domain W3C validator