Theorem mto 106

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 688  intnanr 689  ru 1909  pssn2lp 2118  axnul2 2676  nvel 2682  onprc 2952  ordeleqon 2953  onuninsuc 3071  orduninsuc 3077  snsn0non 3088  nprrel 3171  xp0r 3201  0nelxp 3202  inelv 3290  son2lpi 3393  nfunv 3487  tz7.44lem1 3866  tz7.44-2 3868  0nelqs 4236  sdomn2lp 4409  canth2 4418  rankpw 4608  rankxplim3 4638  kmlem16 4704  cardprc 4784  alephprc 4816  unialeph 4818  cfsuc 4838  nd1 4861  nd2 4862  1pr 5040  1ne0sr 5128  ine0 5357  pnfnre 5419  mnfnre 5420  pnfnemnf 5460  recgt0i 5721  nnunb 5968  nneo 6095  0nrp 6181  indstr 6344  sqr2irr 6610  inelr 6616  climunii 6986  climubi 7040  ivthlem8 7174  ivthlem8OLD 7183  eirrlem5 7285  ruclem36 7439  ruclem37 7440  ruc 7443  tpsex 7498  0ngrp 7937  sinhalfpilem 8511  emnfil 8790  dmadjrnb 9961

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

Copyright terms: Public domain