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 106  mtod 107  nsyld 116  nsyli 120  mth8 122  pm3.48 560  pm5.21nd 684  bibif 685  dn1 779  meredith 931  19.22 1075  equidALT 1163  a4ime 1197  equs5e 1235  sbn 1268  a12stdy1 1411  a12stdy4 1414  a12studyALT 1418  mo 1432  nelneq 1604  nelneq2 1605  necon3ad 1645  necon3bd 1646  mo2icl 1969  sscon 2223  difrab 2325  disjsn 2502  dtru 2831  nsuceq0 3053  limom 3233  relimasn 3517  ndmfv 3856  eqfnfv 3909  eqfnfv2 3911  dff3 3931  canth 4205  tz7.49 4260  oaord 4317  oalimcl 4330  omord2 4334  omcan 4336  oeord 4351  oecan 4352  nneob 4395  omsmo 4397  erdisj 4426  domnsym 4608  ensdomtr 4616  domsdomtr 4621  isfinite1 4677  infsdomnn 4678  pssnn 4681  unfi2 4698  unifi2 4702  supmo 4719  kmlem2 4912  alephord 5025  prub 5252  genpnnp 5262  ltaddpr 5294  prlem936 5309  suppsr3 5378  ssxr 5694  prodge0i 5960  nnge1 6088  supxrun 6253  supxrgtmnf 6260  zeo 6370  uzwo4OLD 6381  irradd 6416  irrmul 6417  uzwo 6582  uzwoOLD 6583  expord 6799  caucvglem6 7365  elcncf 7470  ivthlem6 7491  infdif 7780  infdif2 7781  lmfexlem1 8167  metelcls 8176  bcthlem7 8216  chnlen0 9644  staddi 10454  stadd3i 10456  strlem1 10458  cvnbtwn 10494  atoml2i 10592  atcvatlem 10594  mdsymlem3 10614  pm2.01bd 10722  islfin 10799  fisub 11085  cnfilca 11088  iintlem1 11155  dmsdtriord 11408  ordtypelem7 11433  compfipin0lem 11492  compfipin0 11493  alexsublem4 11499  filrn 11643  filfinnfr 11646  filufint 11659  difxp 11798  fisupg 11839  heiborlem23 12033

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

Copyright terms: Public domain