Theorem con3d 133

Description: A contraposition deduction. Deduction form of con3 134. (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 112	. . 3 |- ( -. -. ps -> ps )
2		con3d.1	. . 3 |- ( ph -> ( ps -> ch ) )
3	1, 2	syl5 32	. 2 |- ( ph -> ( -. -. ps -> ch ) )
4	3	con1d 124	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  134  con3rr3  136  nsyld  140  nsyli  141  mth8  146  pm2.52  155  pm5.21ndd  354  bija  355  con3dimp  441  aleximi  1640  necon1bdOLD  2662  nelcon3d  2792  rexim  2908  spcimegf  3174  spcimedv  3179  rspcimedv  3198  ssneld  3491  sscon  3623  difrab  3757  dtru  4628  otiunsndisj  4743  wereu2  4866  nsuceq0  4948  ndmfv  5880  dff3  6029  soisores  6208  ressuppssdif  6923  tz7.49  7112  oaord  7198  oalimcl  7211  omord2  7218  omcan  7220  omeulem1  7233  oeord  7239  oecan  7240  nnaord  7270  nnmord  7283  nneob  7303  omsmo  7305  domtriord  7665  isinf  7735  pssnn  7740  frfi  7767  fisupg  7770  difinf  7792  supmo  7914  alephord  8459  fin17  8777  isfin7-2  8779  fin1a2lem12  8794  fpwwe2lem13  9023  prub  9375  genpnnp  9386  ltaddpr  9415  prlem936  9428  ltadd2  9691  ltord1  10086  prodge0  10396  ltmul1  10399  lt2msq  10436  nnge1  10569  zeo  10955  irradd  11217  irrmul  11218  supxrun  11518  supxrgtmnf  11532  ssfzoulel  11888  zesq  12271  bccmpl  12369  swrd0  12640  repswswrd  12738  coprm  14223  prmreclem3  14418  vdwnnlem2  14496  latnlej2  15680  mgm2nsgrplem3  16017  f1omvdco2  16452  oddvds  16550  gexdvds  16583  frgpnabl  16858  ablfac1eulem  17102  ablfac1eu  17103  psgnodpm  18602  obselocv  18737  1marepvmarrepid  19055  mdetunilem9  19100  t1conperf  19915  txindislem  20112  fbasrn  20363  isufil2  20387  ufileu  20398  filufint  20399  ufilen  20409  fin1aufil  20411  alexsubALTlem4  20528  ptcmplem2  20531  itg2gt0  22145  cosord  22897  argimgt0  22975  logdivlt  22984  logrec  23129  dcubic  23155  wilthlem2  23321  bposlem3  23539  dchrisum0fno1  23674  usgranloop0  24358  nbgra0nb  24407  nbcusgra  24441  cusgrafi  24460  vdusgra0nedg  24886  usgravd0nedg  24896  usgravd00  24897  2spotmdisj  25046  chnlen0  26340  staddi  27143  stadd3i  27145  strlem1  27147  atoml2i  27280  mul2lt0bi  27547  hasheuni  28069  eulerpartlemb  28285  ballotlemfc0  28409  ballotlemfcc  28410  dfon2lem6  29196  exnel  29211  wfrlem10  29328  sltres  29400  nodenselem4  29420  nofulllem5  29442  waj-ax  29855  wl-ax11-lem3  30003  areacirc  30088  nn0prpwlem  30116  pridlc3  30446  hashgcdeq  31134  afvres  32211  otiunsndisjX  32255  copisnmnd  32450  vk15.4j  33166  isosctrlem1ALT  33602  bj-dtru  34266  lkreqN  34770  atlrelat1  34921  2llnneN  35008  cdlemg4c  36213  mapdh8e  37386  bj-frege52a  37706