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 555  pm5.21nd 678  bibif 679  meredith 921  19.22 1035  a4ime 1156  equs5e 1194  sbn 1226  a12stdy1 1365  a12stdy4 1368  a12studyALT 1372  mo 1386  nelneq 1553  nelneq2 1554  necon3ad 1594  necon3bd 1595  mo2icl 1914  sscon 2161  difrab 2263  disjsn 2431  dtruALT 2738  nsuceq0 3043  limom 3136  relimasn 3409  ndmfv 3730  eqfnfv 3782  dff2 3802  canth 3892  tz7.49 3944  oaord 4165  oalimcl 4178  omord2 4182  omcan 4184  oeord 4199  oecan 4200  nneob 4239  omsmo 4241  erdisj 4270  eceqopreq 4297  domnsym 4443  ensdomtr 4451  domsdomtr 4456  isfinite1 4510  infsdomnn 4511  pssnn 4513  unfi2 4529  unifi2 4533  supmo 4550  kmlem2 4738  alephord 4847  prub 5070  genpnnp 5080  ltaddpr 5112  prlem936 5127  suppsr3 5196  ssxr 5513  prodge0 5776  nnge1t 5891  supxrun 6032  supxrgtmnf 6039  zeot 6146  uzwo4OLD 6158  uzwo 6387  uzwoOLD 6388  expordt 6533  caucvglem6 7098  elcncf 7200  ivthlem6 7221  ivthlem6OLD 7230  infdif 7511  infdif2 7512  lmfexlem1 7891  metelcls 7900  bcthlem7 7939  chnlen0 9283  spansneleqOLD 9410  spansncv 9514  stadd 10083  stadd3 10085  strlem1 10087  cvnbtwnt 10123  atoml2 10218  atcvatlem 10220  mdsymlem3 10240  fisub 10447  cnfilca 10451  iintlem1 10476

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

Copyright terms: Public domain