Theorem con3d 138

Description: A contraposition deduction. Deduction form of con3 139. (Contributed by NM, 10-Jan-1993.)

Hypothesis

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

Assertion

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

Proof of Theorem con3d

Step	Hyp	Ref	Expression
1		notnot2 115	. . 3 |- ( -. -. ps -> ps )
2		con3d.1	. . 3 |- ( ph -> ( ps -> ch ) )
3	1, 2	syl5 33	. 2 |- ( ph -> ( -. -. ps -> ch ) )
4	3	con1d 127	1 |- ( ph -> ( -. ch -> -. ps ) )

Syntax hints:   -. wn 3   -> wi 4

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

This theorem is referenced by:  con3  139  con3rr3  141  nsyld  145  nsyli  146  mth8  149  pm2.52  158  pm5.21ndd  355  bija  356  con3dimp  442  stoic1a  1651  aleximi  1700  necon1bdOLD  2643  nelcon3d  2774  rexim  2890  spcimegf  3160  spcimedv  3165  rspcimedv  3184  ssneld  3466  sscon  3599  difrab  3747  eqoreldif  4038  dtru  4612  otiunsndisj  4723  wereu2  4847  nsuceq0  5519  ndmfv  5902  dff3  6047  soisores  6230  ressuppssdif  6944  wfrlem10  7050  tz7.49  7167  oaord  7253  oalimcl  7266  omord2  7273  omcan  7275  omeulem1  7288  oeord  7294  oecan  7295  nnaord  7325  nnmord  7338  nneob  7358  omsmo  7360  domtriord  7721  isinf  7788  pssnn  7793  frfi  7819  fisupg  7822  difinf  7844  supmo  7969  infmo  8014  fiinfg  8018  alephord  8507  fin17  8825  isfin7-2  8827  fin1a2lem12  8842  fpwwe2lem13  9068  prub  9420  genpnnp  9431  ltaddpr  9460  prlem936  9473  ltadd2  9739  ltord1  10141  prodge0  10453  ltmul1  10456  lt2msq  10492  nnge1  10636  zeo  11022  irradd  11289  irrmul  11290  mul2lt0bi  11403  supxrun  11602  supxrgtmnf  11616  ssfzoulel  12005  zesq  12395  bccmpl  12494  repswswrd  12878  lcmftp  14597  coprm  14645  prmreclem3  14850  vdwnnlem2  14934  latnlej2  16305  mgm2nsgrplem3  16642  f1omvdco2  17077  oddvds  17184  gexdvds  17223  frgpnabl  17499  ablfac1eulem  17693  ablfac1eu  17694  psgnodpm  19143  obselocv  19278  1marepvmarrepid  19587  mdetunilem9  19632  t1conperf  20438  txindislem  20635  fbasrn  20886  isufil2  20910  ufileu  20921  filufint  20922  ufilen  20932  fin1aufil  20934  alexsubALTlem4  21052  ptcmplem2  21055  itg2gt0  22705  cosord  23468  argimgt0  23548  logdivlt  23557  logrec  23687  dcubic  23759  wilthlem2  23981  bposlem3  24201  dchrisum0fno1  24336  usgranloop0  25094  nbgra0nb  25143  nbcusgra  25177  cusgrafi  25196  vdusgra0nedg  25622  usgravd0nedg  25632  usgravd00  25633  2spotmdisj  25782  chnlen0  27083  staddi  27885  stadd3i  27887  strlem1  27889  atoml2i  28022  psgnfzto1stlem  28609  madjusmdetlem1  28649  madjusmdetlem2  28650  hasheuni  28902  sitgaddlemb  29177  eulerpartlemb  29197  ballotlemfc0  29321  ballotlemfcc  29322  dfon2lem6  30429  exnel  30444  sltres  30546  nodenselem4  30566  nofulllem5  30588  nn0prpwlem  30971  waj-ax  31067  bj-dtru  31370  wl-ax11-lem3  31831  poimirlem26  31880  poimirlem28  31882  poimirlem31  31885  areacirc  31951  pridlc3  32220  lkreqN  32655  atlrelat1  32806  2llnneN  32893  cdlemg4c  34098  mapdh8e  35271  hashgcdeq  35995  vk15.4j  36743  isosctrlem1ALT  37192  afvres  38386  otiunsndisjX  38708  fundmge2nop  38724  copisnmnd  39081  dig1  39693