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 1033  necon1ad 1628  necon1bd 1629  sspss 2141  neldif 2161  sspr 2471  sotrieq 2856  limsssuc 3116  tfinds 3156  opelxpex2 3274  funiunfv 3857  pw2en 4432  pssnn 4519  rankr1lem 4653  rankxpsuc 4695  entri 4819  xrlttrit 5533  zeot 6154  om2uzf1o 6246  uzwoOLD 6396  fctop 7600  cctop 7602  eigorth 9703  atssmat 10242

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

Copyright terms: Public domain