Theorem con3d 148

Description: A contraposition deduction. Deduction form of con3 149. (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		notnotr 125	. . 3 |- ( -. -. ps -> ps )
2		con3d.1	. . 3 |- ( ph -> ( ps -> ch ) )
3	1, 2	syl5 34	. 2 |- ( ph -> ( -. -. ps -> ch ) )
4	3	con1d 139	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  149  con3rr3  151  nsyld  154  nsyli  155  mth8  158  pm2.52  167  pm5.21ndd  369  bija  370  con3dimp  457  aleximi  1759  nelcon3d  2909  rexim  3008  spcimegf  3287  spcimedv  3292  rspcimedv  3311  ssneld  3605  sscon  3744  difrab  3901  eqoreldifOLD  4226  disjord  4641  disjiund  4643  dtru  4857  otiunsndisj  4980  wereu2  5111  ndmfv  6218  dff3  6372  soisores  6577  ressuppssdif  7316  wfrlem10  7424  tz7.49  7540  oaord  7627  oalimcl  7640  omord2  7647  omcan  7649  omeulem1  7662  oeord  7668  oecan  7669  nnaord  7699  nnmord  7712  nneob  7732  omsmo  7734  domtriord  8106  isinf  8173  pssnn  8178  frfi  8205  fisupg  8208  difinf  8230  supmo  8358  infmo  8401  fiinfg  8405  alephord  8898  fin17  9216  isfin7-2  9218  fin1a2lem12  9233  fpwwe2lem13  9464  prub  9816  genpnnp  9827  ltaddpr  9856  prlem936  9869  ltadd2  10141  ltord1  10554  prodge0  10870  ltmul1  10873  lt2msq  10908  nnge1  11046  nzadd  11425  zeo  11463  irradd  11812  irrmul  11813  mul2lt0bi  11936  supxrun  12146  supxrgtmnf  12159  ssfzoulel  12562  zesq  12987  bccmpl  13096  fundmge2nop0  13274  repswswrd  13531  s3iunsndisj  13707  lcmftp  15349  prm2orodd  15404  coprm  15423  prmndvdsfaclt  15435  hashgcdeq  15494  prmreclem3  15622  vdwnnlem2  15700  latnlej2  17071  mgm2nsgrplem3  17407  f1omvdco2  17868  oddvds  17966  gexdvds  17999  frgpnabl  18278  ablfac1eulem  18471  ablfac1eu  18472  psgnodpm  19934  obselocv  20072  1marepvmarrepid  20381  mdetunilem9  20426  t1connperf  21239  txindislem  21436  fbasrn  21688  isufil2  21712  ufileu  21723  filufint  21724  ufilen  21734  fin1aufil  21736  alexsubALTlem4  21854  ptcmplem2  21857  itg2gt0  23527  cosord  24278  argimgt0  24358  logdivlt  24367  logrec  24501  dcubic  24573  wilthlem2  24795  bposlem3  25011  dchrisum0fno1  25200  numedglnl  26039  nbumgr  26243  uhgrnbgr0nb  26250  cusgrfi  26354  vtxduhgr0nedg  26388  uhgrvd00  26430  wlkp1lem6  26575  2wspmdisj  27201  chnlen0  28303  staddi  29105  stadd3i  29107  strlem1  29109  atoml2i  29242  psgnfzto1stlem  29850  madjusmdetlem1  29893  madjusmdetlem2  29894  hasheuni  30147  sitgaddlemb  30410  eulerpartlemb  30430  ballotlemfc0  30554  ballotlemfcc  30555  funeldmb  31661  dfon2lem6  31693  exnel  31708  sltres  31815  nosepssdm  31836  nosupbnd1lem1  31854  sletr  31883  nn0prpwlem  32317  waj-ax  32413  bj-dtru  32797  sucneqond  33213  wl-spae  33306  wl-ax11-lem3  33364  matunitlindflem1  33405  poimirlem26  33435  poimirlem28  33437  poimirlem31  33440  areacirc  33505  pridlc3  33872  lkreqN  34457  atlrelat1  34608  2llnneN  34695  cdlemg4c  35900  mapdh8e  37073  vk15.4j  38734  isosctrlem1ALT  39170  afvres  41252  otiunsndisjX  41298  fmtnoinf  41448  copisnmnd  41809  dig1  42402