Theorem mto 120

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 113	. 2 |- (-. ps -> -. ph)
4	1, 3	ax-mp 7	1 |- -. ph

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  intnan 752  intnanr 753  equidqe 1152  nexr 1293  ru 2284  pssn2lpOLD 2542  axnulALT 3258  nvel 3265  nlim0 3536  snsn0non 3599  snsn0nonOLD 3600  snnex 3612  onprc 3676  ordeleqon 3677  onuninsuci 3732  orduninsuc 3736  nprrel 3841  xp0r 3876  0nelxp 3877  iprc 4021  son2lpi 4127  nfunv 4264  tz7.44lem1 4946  tz7.44-2 4948  0nelqs 5168  sdomn2lp 5349  canth2 5359  rankpw 5604  rankxplim3 5634  kmlem16 5738  cardprc 5809  alephprc 5837  unialeph 5839  cfsuc 5859  nd1 5886  nd2 5887  1pr 6065  1ne0sr 6153  ine0 6393  pnfnre 6461  mnfnre 6462  recgt0ii 6787  0nrp 7048  nnunb 7074  nneoi 7204  indstr 7425  sqr2irr 7774  inelr 7780  climunii 8153  climubii 8208  ivthlem8 8345  eirrlem5 8450  egt2OLD 8452  elt3OLD 8453  egt2lt3 8454  ruclem36 8609  ruclem37 8610  ruc 8613  tpsex 8669  0ngrp 9130  vcoprne 9325  sinhalfpilem 9823  emnfil 10065  fsubbas 10073  dmadjrnb 11259  bnj52 12219  bnj521 12314  bnj1221 12788  bnj1419 12909  bnj98 13013  bnj1417 13322  divalglem5 13492  4nprm 13573  nosgnn0i 13792  axsltsolem1 13796  noprc 13808  unnf 13887  unnt 13888  unqsym1 13979  amosym1 13980  inpc 14343  empntop 14580  compfipin0 15118  fbasfip 15238  inficl 15439  fz10 15470  heiborlem14 15650  heiborlem40 15676  rrndm 15697  rusbcALT 16092  compne 16099

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

Copyright terms: Public domain