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  1662  hbn1fw  1691  sp  1728  hbn  1732  spimeh  1734  cbv3hv  1749  ax12  1888  dvelimv  1892  ax9  1902  sbn  2015  sbcom  2042  ax12from12o  2108  ax67  2117  ax67to6  2119  ax467to6  2123  equidqe  2125  equidq  2127  ax11indalem  2149  euor2  2224  moexex  2225  baroco  2262  necon1bi  2502  eueq3  2953  sbc2or  3012  difrab  3455  abvor0  3485  ifeqor  3615  ifan  3617  nelpri  3674  opprc1  3834  opprc2  3835  snexALT  4212  mosubopt  4280  eldifpw  4582  nlimsucg  4649  tfindsg  4667  findsg  4699  soirri  5085  soirriOLD  5090  nfvres  5573  fvco4i  5613  fvmptex  5626  fvopab4ndm  5636  ressnop0  5719  ovprc  5901  ovprc1  5902  ovprc2  5903  ndmovass  6024  ndmovdistr  6025  curry1val  6227  curry2val  6231  eceqoveq  6779  fiprc  6958  sdomirr  7014  domtriord  7023  2pwuninel  7032  mapdom1  7042  card2inf  7285  en2lp  7333  wemapwe  7416  rankxplim3  7567  fidomtri2  7643  alephnbtwn  7714  kmlem2  7793  isfin7-2  8038  dominf  8087  ac6n  8128  alephval2  8210  dominfac  8211  gchdomtri  8267  nlt1pi  8546  adderpq  8596  mulerpq  8597  zeo  10113  fzoval  10892  bcpasc  11349  hasheq0  11369  hashbc  11407  prmreclem4  12982  ressinbas  13220  natfval  13836  fucbas  13850  fuchom  13851  homarcl  13876  arwval  13891  coafval  13912  grpidval  14400  symgbas  14788  efgval  15042  gsum2d  15239  psrvscafval  16151  tgdif0  16746  resstopn  16932  cfinfil  17604  pcofval  18524  i1fima2  19050  i1fd  19052  itgeq2  19148  ibladdlem  19190  avril1  20852  nmobndseqi  21373  nonbooli  22246  chpssati  22959  ballotlem2  23063  ballotlemfp1  23066  ballotlem4  23073  ballotlemirc  23106  xrge00  23326  xrge0neqmnf  23345  hasheuni  23468  rdgprc0  24221  distel  24231  predpoirr  24268  predfrirr  24269  linedegen  24838  ordcmp  24958  ibladdnclem  25007  diaimi  25091  evpexun  25101  frinfm  26519  jm2.22  27191  pm10.251  27658  ax4567to6  27707  infrglb  27825  stirlinglem5  27930  ndmafv  28108  nfunsnafv  28110  afvprc  28112  afvnufveq  28115  aovprc  28156  ndmaovass  28174  ndmaovdistr  28175  uvtx01vtx  28305  frgra2v  28423  en3lpVD  28937  a9e2ndeqVD  29001  2sb5ndVD  29002  a9e2ndeqALT  29024  2sb5ndALT  29025  bnj1143  29138  cbv3hvNEW7  29423  dvelimvNEW7  29439  ax9NEW7  29445  sbnNEW7  29537  sbcomwAUX7  29562  sbcomOLD7  29709  ax12conj2  29730  a12study8  29741  ax10lem17ALT  29745  a12lem2  29753  ax9lem1  29762  ax9lem3  29764  ax9lem6  29767  ax9lem8  29769  ax9lem12  29773  ax9lem13  29774  ax9lem17  29778  ax9vax9  29780  hdmap1eulem  32636  hdmapevec  32650
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator