Theorem mto 105

Description: The rule of modus tollens.

Hypotheses

Ref	Expression
mto.1	|- -. ps
mto.2	|- (ph -> ps)

Assertion

Ref	Expression
mto	|- -. ph

Proof of Theorem mto

Step	Hyp	Ref	Expression
1		mto.1	. 2 |- -. ps
2		mto.2	. . 3 |- (ph -> ps)
3	2	con3i 98	. 2 |- (-. ps -> -. ph)
4	1, 3	ax-mp 7	1 |- -. ph

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  intnan 695  intnanr 696  ru 1984  pssn2lp 2199  axnul2 2782  nvel 2788  snsn0non 3088  snnex 3100  onprc 3143  ordeleqon 3144  onuninsuci 3194  orduninsuc 3197  nprrel 3292  xp0r 3325  0nelxp 3326  iprc 3449  son2lpi 3536  nfunv 3651  tz7.44lem1 4228  tz7.44-2 4230  0nelqs 4439  sdomn2lp 4620  canth2 4629  rankpw 4830  rankxplim3 4860  kmlem16 4926  cardprc 5011  alephprc 5043  unialeph 5045  cfsuc 5065  nd1 5092  nd2 5093  1pr 5271  1ne0sr 5359  ine0 5588  pnfnre 5650  mnfnre 5651  recgt0ii 5954  0nrp 6212  nnunb 6238  nneoi 6368  indstr 6588  sqr2irr 6930  inelr 6936  climunii 7301  climubii 7356  ivthlem8 7493  eirrlem5 7598  egt2OLD 7600  elt3OLD 7601  egt2lt3 7602  ruclem36 7757  ruclem37 7758  ruc 7761  tpsex 7817  0ngrp 8268  vcoprne 8445  sinhalfpilem 8946  dmadjrnb 10110  inpc 10867  empntop 11007  emnfil 11078  nexnoti 11392  compfipin0 11493  fbasfip 11627  fsubbas 11630  inficl 11849  heiborlem14 12024  heiborlem40 12050  rrndm 12071

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

Copyright terms: Public domain