Theorem con3d 127

Description: A contraposition deduction. (Contributed by NM, 5-Aug-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 106	. . 3 |- ( -. -. ps -> ps )
2		con3d.1	. . 3 |- ( ph -> ( ps -> ch ) )
3	1, 2	syl5 30	. 2 |- ( ph -> ( -. -. ps -> ch ) )
4	3	con1d 118	1 |- ( ph -> ( -. ch -> -. ps ) )

Syntax hints:   -. wn 3   -> wi 4

This theorem is referenced by:  con3  128  con3rr3  130  nsyld  134  nsyli  135  mth8  140  pm2.52  149  pm5.21ndd  344  bija  345  con3and  429  ax12bOLD  1698  spimeOLD  1957  ax12olem1OLD  1977  mo  2276  necon1bd  2635  rexim  2770  spcimegf  2990  spcimedv  2995  rspcimedv  3014  ssneld  3310  sscon  3441  difrab  3575  dtru  4350  wereu2  4539  nsuceq0  4621  ndmfv  5714  dff3  5841  soisores  6006  tz7.49  6661  oaord  6749  oalimcl  6762  omord2  6769  omcan  6771  omeulem1  6784  oeord  6790  oecan  6791  nnaord  6821  nnmord  6834  nneob  6854  omsmo  6856  domtriord  7212  isinf  7281  pssnn  7286  frfi  7311  fisupg  7314  difinf  7336  supmo  7413  alephord  7912  fin17  8230  isfin7-2  8232  fin1a2lem12  8247  fpwwe2lem13  8473  prub  8827  genpnnp  8838  ltaddpr  8867  prlem936  8880  ltadd2  9133  ltord1  9509  prodge0  9813  ltmul1  9816  lt2msq  9850  nnge1  9982  zeo  10311  irradd  10554  irrmul  10555  supxrun  10850  supxrgtmnf  10864  zesq  11457  bccmpl  11555  coprm  13055  prmreclem3  13241  vdwnnlem2  13319  latnlej2  14455  oddvds  15140  gexdvds  15173  frgpnabl  15441  ablfac1eulem  15585  ablfac1eu  15586  obselocv  16910  t1conperf  17452  txindislem  17618  fbasrn  17869  isufil2  17893  ufileu  17904  filufint  17905  ufilen  17915  fin1aufil  17917  alexsubALTlem4  18034  ptcmplem2  18037  itg2gt0  19605  cosord  20387  argimgt0  20460  logdivlt  20469  logrec  20614  dcubic  20639  wilthlem2  20805  bposlem3  21023  dchrisum0fno1  21158  usgranloop0  21353  nbgra0nb  21394  nbcusgra  21425  cusgrafi  21444  vdusgra0nedg  21632  usgravd0nedg  21636  chnlen0  22899  staddi  23702  stadd3i  23704  strlem1  23706  atoml2i  23839  hasheuni  24428  sibfof  24607  ballotlemfc0  24703  ballotlemfcc  24704  dfon2lem6  25358  exnel  25373  wfrlem10  25479  sltres  25532  nodenselem4  25552  nofulllem5  25574  waj-ax  26068  areacirc  26187  nn0prpwlem  26215  pridlc3  26573  f1omvdco2  27259  hashgcdeq  27385  pm10.56  27433  afvres  27903  otiunsndisj  27954  otiunsndisjX  27955  swrd0  28002  swrdccat3b  28031  2spotmdisj  28171  vk15.4j  28323  spimeNEW7  29215  lkreqN  29653  atlrelat1  29804  2llnneN  29891  cdlemg4c  31094  mapdh8e  32267

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