Theorem con3d 133

Description: A contraposition deduction. (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  1632  moOLD  2327  necon1bdOLD  2686  rexim  2929  spcimegf  3192  spcimedv  3197  rspcimedv  3216  ssneld  3506  sscon  3638  difrab  3772  dtru  4638  otiunsndisj  4753  wereu2  4876  nsuceq0  4958  ndmfv  5888  dff3  6032  soisores  6209  ressuppssdif  6918  tz7.49  7107  oaord  7193  oalimcl  7206  omord2  7213  omcan  7215  omeulem1  7228  oeord  7234  oecan  7235  nnaord  7265  nnmord  7278  nneob  7298  omsmo  7300  domtriord  7660  isinf  7730  pssnn  7735  frfi  7761  fisupg  7764  difinf  7786  supmo  7908  alephord  8452  fin17  8770  isfin7-2  8772  fin1a2lem12  8787  fpwwe2lem13  9016  prub  9368  genpnnp  9379  ltaddpr  9408  prlem936  9421  ltadd2  9684  ltord1  10075  prodge0  10385  ltmul1  10388  lt2msq  10425  nnge1  10558  zeo  10942  irradd  11202  irrmul  11203  supxrun  11503  supxrgtmnf  11517  ssfzoulel  11870  zesq  12253  bccmpl  12351  swrd0  12617  repswswrd  12715  coprm  14096  prmreclem3  14291  vdwnnlem2  14369  latnlej2  15554  f1omvdco2  16269  oddvds  16367  gexdvds  16400  frgpnabl  16670  ablfac1eulem  16913  ablfac1eu  16914  psgnodpm  18391  obselocv  18526  1marepvmarrepid  18844  mdetunilem9  18889  t1conperf  19703  txindislem  19869  fbasrn  20120  isufil2  20144  ufileu  20155  filufint  20156  ufilen  20166  fin1aufil  20168  alexsubALTlem4  20285  ptcmplem2  20288  itg2gt0  21902  cosord  22652  argimgt0  22725  logdivlt  22734  logrec  22879  dcubic  22905  wilthlem2  23071  bposlem3  23289  dchrisum0fno1  23424  ncolne2  23720  ncolncol  23739  symquadlem  23774  midexlem  23777  usgranloop0  24056  nbgra0nb  24105  nbcusgra  24139  cusgrafi  24158  vdusgra0nedg  24584  usgravd0nedg  24594  usgravd00  24595  2spotmdisj  24745  chnlen0  26038  staddi  26841  stadd3i  26843  strlem1  26845  atoml2i  26978  ofpreima2  27180  mul2lt0bi  27237  orngsqr  27457  hasheuni  27731  eulerpartlemb  27947  ballotlemfc0  28071  ballotlemfcc  28072  dfon2lem6  28797  exnel  28812  wfrlem10  28929  sltres  29001  nodenselem4  29021  nofulllem5  29043  waj-ax  29456  wl-ax11-lem3  29604  areacirc  29689  nn0prpwlem  29717  pridlc3  30073  hashgcdeq  30763  afvres  31724  otiunsndisjX  31768  vk15.4j  32377  isosctrlem1ALT  32814  bj-dtru  33464  lkreqN  33967  atlrelat1  34118  2llnneN  34205  cdlemg4c  35408  mapdh8e  36581