Theorem con1d 93

Description: A contraposition deduction.

Hypothesis

Ref	Expression
con1d.1	|- (ph -> (-. ps -> ch))

Assertion

Ref	Expression
con1d	|- (ph -> (-. ch -> ps))

Proof of Theorem con1d

Step	Hyp	Ref	Expression
1		con1d.1	. 2 |- (ph -> (-. ps -> ch))
2		con1 92	. 2 |- ((-. ps -> ch) -> (-. ch -> ps))
3	1, 2	syl 10	1 |- (ph -> (-. ch -> ps))

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  pm2.24d 105  mt3i 113  mt3d 114  impt 141  dedlem0b 760  19.9t 1034  necon1ad 1630  necon1bd 1631  sspss 2143  neldif 2163  sspr 2473  sotrieq 2858  limsssuc 3118  tfinds 3158  opelxpex2 3276  funiunfv 3863  pw2en 4439  pssnn 4526  rankr1lem 4660  rankxpsuc 4702  entri 4826  xrlttrit 5539  zeot 6160  om2uzf1o 6256  uzwoOLD 6406  fctop 7629  cctop 7631  eigorth 9754  atssmat 10296

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

Copyright terms: Public domain