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

Theorem mt2d 131
 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 129 . 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  132  nsyl3  133  tz7.44-3  7489  sdomdomtr  8078  domsdomtr  8080  infdif  9016  ackbij1b  9046  isf32lem5  9164  alephreg  9389  cfpwsdom  9391  inar1  9582  tskcard  9588  npomex  9803  recnz  11437  rpnnen1lem5  11803  rpnnen1lem5OLD  11809  fznuz  12406  uznfz  12407  seqcoll2  13232  ramub1lem1  15711  pgpfac1lem1  18454  lsppratlem6  19133  nconnsubb  21207  iunconnlem  21211  clsconn  21214  xkohaus  21437  reconnlem1  22610  ivthlem2  23202  perfectlem1  24935  lgseisenlem1  25081  ex-natded5.8-2  27241  oddpwdc  30390  erdszelem9  31155  relowlpssretop  33183  sucneqond  33184  heiborlem8  33588  lcvntr  34132  ncvr1  34378  llnneat  34619  2atnelpln  34649  lplnneat  34650  lplnnelln  34651  3atnelvolN  34691  lvolneatN  34693  lvolnelln  34694  lvolnelpln  34695  lplncvrlvol  34721  4atexlemntlpq  35173  cdleme0nex  35396
 Copyright terms: Public domain W3C validator