Theorem con3d 87

Description: A contraposition deduction.

Hypothesis

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

Assertion

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

Proof of Theorem con3d

Step	Hyp	Ref	Expression
1		con3d.1	. 2 |- (ph -> (ps -> ch))
2		con3 86	. 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:  mtoi 94  mtod 95  nsyli 106  mth8 108  pm3.48 430  meredith 644  19.22 722  del40 839  del41 840  del42 841  a4c 843  sbn1 880  sbn2 881  hbsb4 905  mo 1020  clneq 1168  clneq2 1169  mo2icl 1434  sscon 1599  difrab 1695  disjpss 1738  pssdifn0 1750  disjsn 1836  nsuceq0 2306  limom 2387  peano5 2394  imasn 2616  ndmfv 2848  cleqfv 2880  canth 2945  tz7.49 2997  oaord 3149  oalimcl 3162  nnmord 3189  nnmcan 3190  omsmo 3196  erdisj 3223  eceqopreq 3249  domnsym 3365  ensdomtr 3372  domsdomtr 3374  isfinite1 3425  infsdomnn 3426  pssnn 3428  unfi2 3442  kmlem2 3581  kmlem8 3587  alephord 3680  prub 3892  genpnnp 3902  ltaddpr 3934  prlem936 3949  suppsr3 4018  nnge1t 4439  uzwo 4605  nnwoOLD 4608  infxpidmlem10 4942  infdif 4948  chnlen0 5369  h1dn0 5457  spansneleq 5475  h1datom 5483  spansncv 5542  stadd 5687  stadd3 5689  strlem1 5691  cvnbtwnt 5718  atcvatlem 5770  mdsymlem3 5778

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

metamath.org