MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  con3d Structured version   Unicode version

Theorem con3d 128
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
StepHypRef Expression
1 notnot2 107 . . 3  |-  ( -. 
-.  ps  ->  ps )
2 con3d.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2syl5 31 . 2  |-  ( ph  ->  ( -.  -.  ps  ->  ch ) )
43con1d 119 1  |-  ( ph  ->  ( -.  ch  ->  -. 
ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  con3  129  con3rr3  131  nsyld  135  nsyli  136  mth8  141  pm2.52  150  pm5.21ndd  345  bija  346  con3and  430  ax12bOLD  1703  spimeOLD  1960  ax12olem1OLD  2012  mo  2305  necon1bd  2674  rexim  2812  spcimegf  3032  spcimedv  3037  rspcimedv  3056  ssneld  3352  sscon  3483  difrab  3617  dtru  4392  wereu2  4581  nsuceq0  4663  ndmfv  5757  dff3  5884  soisores  6049  tz7.49  6704  oaord  6792  oalimcl  6805  omord2  6812  omcan  6814  omeulem1  6827  oeord  6833  oecan  6834  nnaord  6864  nnmord  6877  nneob  6897  omsmo  6899  domtriord  7255  isinf  7324  pssnn  7329  frfi  7354  fisupg  7357  difinf  7379  supmo  7459  alephord  7958  fin17  8276  isfin7-2  8278  fin1a2lem12  8293  fpwwe2lem13  8519  prub  8873  genpnnp  8884  ltaddpr  8913  prlem936  8926  ltadd2  9179  ltord1  9555  prodge0  9859  ltmul1  9862  lt2msq  9896  nnge1  10028  zeo  10357  irradd  10600  irrmul  10601  supxrun  10896  supxrgtmnf  10910  zesq  11504  bccmpl  11602  coprm  13102  prmreclem3  13288  vdwnnlem2  13366  latnlej2  14502  oddvds  15187  gexdvds  15220  frgpnabl  15488  ablfac1eulem  15632  ablfac1eu  15633  obselocv  16957  t1conperf  17501  txindislem  17667  fbasrn  17918  isufil2  17942  ufileu  17953  filufint  17954  ufilen  17964  fin1aufil  17966  alexsubALTlem4  18083  ptcmplem2  18086  itg2gt0  19654  cosord  20436  argimgt0  20509  logdivlt  20518  logrec  20663  dcubic  20688  wilthlem2  20854  bposlem3  21072  dchrisum0fno1  21207  usgranloop0  21402  nbgra0nb  21443  nbcusgra  21474  cusgrafi  21493  vdusgra0nedg  21681  usgravd0nedg  21685  chnlen0  22948  staddi  23751  stadd3i  23753  strlem1  23755  atoml2i  23888  hasheuni  24477  sibfof  24656  ballotlemfc0  24752  ballotlemfcc  24753  dfon2lem6  25417  exnel  25432  wfrlem10  25549  sltres  25621  nodenselem4  25641  nofulllem5  25663  waj-ax  26166  areacirc  26299  nn0prpwlem  26327  pridlc3  26685  f1omvdco2  27370  hashgcdeq  27496  pm10.56  27544  afvres  28014  otiunsndisj  28069  otiunsndisjX  28070  swrd0  28205  swrdvalodmlem1  28209  usgravd00  28424  2spotmdisj  28519  vk15.4j  28674  isosctrlem1ALT  29108  spimeNEW7  29571  lkreqN  30030  atlrelat1  30181  2llnneN  30268  cdlemg4c  31471  mapdh8e  32644
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator