Theorem con1d 85

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 84	. 2 |- ((-. ps -> ch) -> (-. ch -> ps))
3	1, 2	syl 12	1 |- (ph -> (-. ch -> ps))

Syntax hints:  -. wn 1   -> wi 2

This theorem is referenced by:  mt3i 100  mt3d 101  impt 122  dedlem0b 568  19.9t 719  sspss 1569  neldif 1594  sotrieq 2149  onmindif2 2313  limsssuc 2362  tfinds 2401  fvclss 2907  pw2en 3348  pssnn 3428  rankr1lem 3517  aceq5lem4 3561  entri 3645  nnleltp1t 4448  uzwo 4605  nnwoOLD 4608  om2uzf1o 4656  sqr0 4730  h1datom 5483

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

metamath.org