Theorem con3d 95

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 94	. 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:  mtoi 107  mtod 108  nsyld 117  nsyli 121  mth8 123  pm3.48 559  pm5.21nd 682  bibif 683  meredith 926  19.22 1041  a4ime 1162  equs5e 1200  sbn 1233  a12stdy1 1374  a12stdy4 1377  a12studyALT 1381  mo 1395  nelneq 1564  nelneq2 1565  necon3ad 1605  necon3bd 1606  mo2icl 1926  sscon 2174  difrab 2276  disjsn 2445  dtruALT 2754  nsuceq0 3059  limom 3152  relimasn 3431  ndmfv 3751  eqfnfv 3803  dff2 3823  canth 3913  tz7.49 3965  oaord 4187  oalimcl 4200  omord2 4204  omcan 4206  oeord 4221  oecan 4222  nneob 4261  omsmo 4263  erdisj 4292  eceqopreq 4319  domnsym 4469  ensdomtr 4477  domsdomtr 4482  isfinite1 4539  isfinite1OLD 4540  infsdomnn 4541  pssnn 4544  unfi2 4565  unfi2OLD 4566  unifi2OLD 4571  supmo 4585  kmlem2 4776  alephord 4886  prub 5110  genpnnp 5120  ltaddpr 5152  prlem936 5167  suppsr3 5236  ssxr 5552  prodge0 5822  nnge1t 5945  supxrun 6087  supxrgtmnf 6094  zeot 6201  uzwo4OLD 6212  uzwo 6456  uzwoOLD 6457  expordt 6603  caucvglem6 7162  elcncf 7265  ivthlem6 7286  infdif 7569  infdif2 7570  lmfexlem1 7953  metelcls 7962  bcthlem7 8002  chnlen0 9363  stadd 10168  stadd3 10170  strlem1 10172  cvnbtwnt 10208  atoml2 10305  atcvatlem 10307  mdsymlem3 10327  fisub 10558  cnfilca 10562  iintlem1 10603

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

Copyright terms: Public domain