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 761  19.9t 1035  necon1ad 1631  necon1bd 1632  sspss 2145  neldif 2165  sspr 2475  sotrieq 2861  limsssuc 3121  tfinds 3161  opelxpex2 3279  funiunfv 3866  pw2en 4446  pssnn 4534  rankr1lem 4673  rankxpsuc 4715  entri 4839  xrlttrit 5552  zeot 6199  om2uzf1o 6301  uzwoOLD 6456  fctopOLD 7650  cctop 7652  eigorth 9763  atssmat 10305

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

Copyright terms: Public domain