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

Theorem con3i 127
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 19 . 2  |-  ( -. 
ps  ->  -.  ps )
2 con3i.a . 2  |-  ( ph  ->  ps )
31, 2nsyl 113 1  |-  ( -. 
ps  ->  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm2.51  145  pm2.65i  165  pm5.21ni  341  pm2.45  386  pm2.46  387  pm5.14  856  con3th  924  cadan  1382  rb-ax2  1508  rb-ax4  1510  equid  1644  hbn1fw  1679  sp  1716  hbn  1720  spimeh  1722  cbv3hv  1737  dvelimv  1879  ax9  1889  sbn  2002  sbcom  2029  ax12  2095  ax67  2104  ax67to6  2106  ax467to6  2110  equidqe  2112  equidq  2114  ax11indalem  2136  euor2  2211  moexex  2212  baroco  2249  necon1bi  2489  eueq3  2940  sbc2or  2999  difrab  3442  abvor0  3472  ifeqor  3602  ifan  3604  nelpri  3661  opprc1  3818  opprc2  3819  snexALT  4196  mosubopt  4264  eldifpw  4566  nlimsucg  4633  tfindsg  4651  findsg  4683  soirri  5069  soirriOLD  5074  nfvres  5557  fvco4i  5597  fvmptex  5610  fvopab4ndm  5620  ressnop0  5703  ovprc  5885  ovprc1  5886  ovprc2  5887  ndmovass  6008  ndmovdistr  6009  curry1val  6211  curry2val  6215  eceqoveq  6763  fiprc  6942  sdomirr  6998  domtriord  7007  2pwuninel  7016  mapdom1  7026  card2inf  7269  en2lp  7317  wemapwe  7400  rankxplim3  7551  fidomtri2  7627  alephnbtwn  7698  kmlem2  7777  isfin7-2  8022  dominf  8071  ac6n  8112  alephval2  8194  dominfac  8195  gchdomtri  8251  nlt1pi  8530  adderpq  8580  mulerpq  8581  zeo  10097  fzoval  10876  bcpasc  11333  hasheq0  11353  hashbc  11391  prmreclem4  12966  ressinbas  13204  natfval  13820  fucbas  13834  fuchom  13835  homarcl  13860  arwval  13875  coafval  13896  grpidval  14384  symgbas  14772  efgval  15026  gsum2d  15223  psrvscafval  16135  tgdif0  16730  resstopn  16916  cfinfil  17588  pcofval  18508  i1fima2  19034  i1fd  19036  itgeq2  19132  ibladdlem  19174  avril1  20836  nmobndseqi  21357  nonbooli  22230  chpssati  22943  ballotlem2  23047  ballotlemfp1  23050  ballotlem4  23057  ballotlemirc  23090  xrge00  23311  xrge0neqmnf  23330  hasheuni  23453  rdgprc0  24150  distel  24160  predpoirr  24197  predfrirr  24198  funpartfv  24483  linedegen  24766  ordcmp  24886  diaimi  24988  evpexun  24998  frinfm  26416  jm2.22  27088  pm10.251  27555  ax4567to6  27604  infrglb  27722  stirlinglem5  27827  ndmafv  28003  nfunsnafv  28005  afvprc  28007  afvnufveq  28010  aovprc  28048  ndmaovass  28066  ndmaovdistr  28067  uvtx01vtx  28164  frgra2v  28177  en3lpVD  28621  a9e2ndeqVD  28685  2sb5ndVD  28686  a9e2ndeqALT  28708  2sb5ndALT  28709  bnj1143  28822  ax12conj2  29108  a12study8  29119  ax10lem17ALT  29123  a12lem2  29131  ax9lem1  29140  ax9lem3  29142  ax9lem6  29145  ax9lem8  29147  ax9lem12  29151  ax9lem13  29152  ax9lem17  29156  ax9vax9  29158  hdmap1eulem  32014  hdmapevec  32028
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator