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

Theorem con3i 140
Description: A contraposition inference. Inference associated with con3 139. Its associated inference is mto 179. (Contributed by NM, 3-Jan-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 22 . 2  |-  ( -. 
ps  ->  -.  ps )
2 con3i.a . 2  |-  ( ph  ->  ps )
31, 2nsyl 124 1  |-  ( -. 
ps  ->  -.  ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  pm2.51  156  pm2.65i  176  pm5.21ni  353  pm2.45  398  pm2.46  399  nbiorOLD  869  pm5.14  894  con3th  966  rb-ax2  1630  rb-ax4  1632  stoic1aOLD  1650  ax13  2108  sbequi  2175  euor2  2315  baroco  2373  necon3bi  2622  prcnel  3031  eueq3  3183  sbc2or  3246  sbcimdv  3299  sbcrext  3311  difrab  3685  abvor0  3718  csbprc  3738  sbcel12  3740  sbcne12  3743  sbcel2  3746  ifeqor  3893  ifan  3895  nelpri  3956  nelprd  3957  opprc1  4148  opprc2  4149  sbcbr123  4413  snexALT  4548  mosubopt  4656  csbopab  4690  csbxp  4873  soirri  5183  predpoirr  5365  predfrirr  5366  csbiota  5532  nfvres  5850  fvco4i  5898  fvmptex  5915  fvopab4ndm  5927  ressnop0  6025  csbriota  6218  ovprc  6274  ovprc1  6275  ovprc2  6276  ndmovass  6410  ndmovdistr  6411  eldifpw  6556  nlimsucg  6622  tfindsg  6640  findsg  6673  curry1val  6839  curry2val  6843  extmptsuppeq  6889  funsssuppss  6891  eceqoveq  7418  fiprc  7600  sdomirr  7657  domtriord  7666  2pwuninel  7675  mapdom1  7685  nfielex  7748  relprcnfsupp  7834  supval2  7917  wemapso2  8016  card2inf  8018  en2lp  8066  wemapwe  8149  rankxplim3  8299  fidomtri2  8375  alephnbtwn  8448  kmlem2  8527  isfin7-2  8772  dominf  8821  ac6n  8861  alephval2  8943  dominfac  8944  axpowndlem3  8970  gchdomtri  9000  nlt1pi  9277  adderpq  9327  mulerpq  9328  zeo  10967  xrge0neqmnf  11683  fzoval  11867  bcpasc  12451  hashnemnf  12472  hasheq0  12489  hashunx  12510  hashbc  12559  prmreclem4  14801  ressinbas  15123  natfval  15789  fucbas  15803  fuchom  15804  homarcl  15861  arwval  15876  coafval  15897  grpidval  16441  symgbas  16959  efgval  17305  gsum2dlem1  17540  gsum2dlem2  17541  dprddomprc  17570  dprdval0prc  17572  psrvscafval  18552  mavmul0g  19515  mdetralt  19570  mdetunilem9  19582  tgdif0  19945  resstopn  20139  cfinfil  20845  pcofval  21978  i1fima2  22574  i1fd  22576  itgeq2  22672  ibladdlem  22714  cusgrafi  25147  uvtx01vtx  25157  frgra2v  25664  2spotiundisj  25727  numclwwlkdisj  25745  avril1  25837  nmobndseqi  26357  nonbooli  27241  chpssati  27953  hasheuni  28853  inelpisys  28923  ddemeas  29006  bnj1143  29549  rdgprc0  30386  distel  30396  linedegen  30854  ordcmp  31051  bj-con3thALT  31099  bj-babygodel  31130  bj-nexrt  31186  bj-csbprc  31422  bj-projval  31501  onsucuni3  31677  finxpnom  31700  wl-naev  31769  wl-ax11-lem8  31829  poimirlem26  31873  poimirlem27  31874  poimirlem31  31878  cnambfre  31896  itg2addnclem3  31902  ibladdnclem  31905  frinfm  31969  tsbi3  32284  ax13fromc9  32388  axc711  32397  axc711toc7  32399  axc5c711toc7  32403  equidqe  32405  equidq  32407  ax12indalem  32428  hdmap1eulem  35304  hdmapevec  35318  jm2.22  35763  rp-fakeimass  36069  nanorxor  36566  binomcxplemfrat  36613  binomcxplemradcnv  36614  pm10.251  36622  axc5c4c711toc7  36668  en3lpVD  37157  ax6e2ndeqVD  37222  2sb5ndVD  37223  ax6e2ndeqALT  37244  2sb5ndALT  37245  sineq0ALT  37250  fzdifsuc2  37427  infrglbOLD  37552  cncfiooicc  37655  itgcoscmulx  37729  sge0sn  38072  iundjiunlem  38148  isomenndlem  38202  hoidmvlelem2  38265  nabctnabc  38333  ndmafv  38455  nfunsnafv  38457  afvprc  38459  afvnufveq  38462  aovprc  38503  ndmaovass  38521  ndmaovdistr  38522  fundmge2nop  38832  fun2dmnop  38833
  Copyright terms: Public domain W3C validator