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

Theorem con3i 130
Description: A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 20-Jun-2013.)
Hypothesis
Ref Expression
con3i.a  |-  ( ph  ->  ps )
Assertion
Ref Expression
con3i  |-  ( -. 
ps  ->  -.  ph )

Proof of Theorem con3i
StepHypRef Expression
1 id 21 . 2  |-  ( -. 
ps  ->  -.  ps )
2 con3i.a . 2  |-  ( ph  ->  ps )
31, 2nsyl 116 1  |-  ( -. 
ps  ->  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm2.51  148  pm2.65i  168  pm5.21ni  343  pm2.45  388  pm2.46  389  pm5.14  858  con3th  926  cadan  1402  rb-ax2  1528  rb-ax4  1530  equidOLD  1690  hbn1fwOLD  1721  spOLD  1765  hbnOLD  1803  spimehOLD  1841  cbv3hvOLD  1880  ax12  2020  ax12OLD  2021  dvelimvOLD  2029  ax9OLD  2034  sbnOLD  2133  sbcom  2166  sbcomOLD  2167  ax12from12o  2235  ax67  2244  ax67to6  2246  ax467to6  2250  equidqe  2252  equidq  2254  ax11indalem  2276  euor2  2351  moexex  2352  baroco  2389  necon1bi  2649  eueq3  3111  sbc2or  3171  difrab  3617  abvor0  3647  ifeqor  3778  ifan  3780  nelpri  3837  opprc1  4008  opprc2  4009  snexALT  4387  mosubopt  4456  eldifpw  4757  nlimsucg  4824  tfindsg  4842  findsg  4874  soirri  5262  soirriOLD  5267  nfvres  5762  fvco4i  5803  fvmptex  5817  fvopab4ndm  5827  ressnop0  5915  ovprc  6110  ovprc1  6111  ovprc2  6112  ndmovass  6237  ndmovdistr  6238  curry1val  6441  curry2val  6445  eceqoveq  7011  fiprc  7190  sdomirr  7246  domtriord  7255  2pwuninel  7264  mapdom1  7274  nfielex  7339  card2inf  7525  en2lp  7573  wemapwe  7656  rankxplim3  7807  fidomtri2  7883  alephnbtwn  7954  kmlem2  8033  isfin7-2  8278  dominf  8327  ac6n  8367  alephval2  8449  dominfac  8450  gchdomtri  8506  nlt1pi  8785  adderpq  8835  mulerpq  8836  zeo  10357  fzoval  11143  bcpasc  11614  hashnemnf  11630  hasheq0  11646  hashunx  11662  hashbc  11704  prmreclem4  13289  ressinbas  13527  natfval  14145  fucbas  14159  fuchom  14160  homarcl  14185  arwval  14200  coafval  14221  grpidval  14709  symgbas  15097  efgval  15351  gsum2d  15548  psrvscafval  16456  tgdif0  17059  resstopn  17252  cfinfil  17927  pcofval  19037  i1fima2  19573  i1fd  19575  itgeq2  19671  ibladdlem  19713  cusgrafi  21493  uvtx01vtx  21503  avril1  21759  nmobndseqi  22282  nonbooli  23155  chpssati  23868  xrge0neqmnf  24214  hasheuni  24477  rdgprc0  25423  distel  25433  predpoirr  25474  predfrirr  25475  linedegen  26079  ordcmp  26199  cnambfre  26257  itg2addnclem3  26260  ibladdnclem  26263  frinfm  26439  jm2.22  27068  pm10.251  27534  ax4567to6  27583  infrglb  27700  ndmafv  27982  nfunsnafv  27984  afvprc  27986  afvnufveq  27989  aovprc  28030  ndmaovass  28048  ndmaovdistr  28049  nelprd  28057  frgra2v  28451  2spotiundisj  28513  en3lpVD  29019  a9e2ndeqVD  29083  2sb5ndVD  29084  a9e2ndeqALT  29105  2sb5ndALT  29106  sineq0ALT  29111  bnj1143  29223  cbv3hvNEW7  29508  dvelimvNEW7  29524  ax9NEW7  29530  sbnNEW7  29624  sbcomwAUX7  29650  ax7w15lemxAUX7  29728  ax7w15AUX7  29730  sbcomOLD7  29817  hdmap1eulem  32684  hdmapevec  32698
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator