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 557  pm5.21nd 680  bibif 681  meredith 924  19.22 1039  a4ime 1160  equs5e 1198  sbn 1231  a12stdy1 1372  a12stdy4 1375  a12studyALT 1379  mo 1393  nelneq 1561  nelneq2 1562  necon3ad 1602  necon3bd 1603  mo2icl 1923  sscon 2171  difrab 2273  disjsn 2441  dtruALT 2748  nsuceq0 3053  limom 3146  relimasn 3425  ndmfv 3745  eqfnfv 3797  dff2 3817  canth 3907  tz7.49 3959  oaord 4181  oalimcl 4194  omord2 4198  omcan 4200  oeord 4215  oecan 4216  nneob 4255  omsmo 4257  erdisj 4286  eceqopreq 4313  domnsym 4463  ensdomtr 4471  domsdomtr 4476  isfinite1OLD 4531  infsdomnn 4532  pssnn 4534  unfi2 4553  unifi2 4558  supmo 4576  kmlem2 4766  alephord 4875  prub 5098  genpnnp 5108  ltaddpr 5140  prlem936 5155  suppsr3 5224  ssxr 5540  prodge0 5820  nnge1t 5943  supxrun 6085  supxrgtmnf 6092  zeot 6199  uzwo4OLD 6210  uzwo 6455  uzwoOLD 6456  expordt 6602  caucvglem6 7162  elcncf 7265  ivthlem6 7286  infdif 7568  infdif2 7569  lmfexlem1 7956  metelcls 7965  bcthlem7 8005  chnlen0 9368  stadd 10173  stadd3 10175  strlem1 10177  cvnbtwnt 10213  atoml2 10310  atcvatlem 10312  mdsymlem3 10332  fisub 10576  fisubOLD 10577  cnfilca 10583  cnfilcaOLD 10584  iintlem1 10632

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

Copyright terms: Public domain