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

Theorem con3i 135
Description: A contraposition inference. Inference associated with con3 134. Its associated inference is mto 176. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 20-Jun-2013.)
Hypothesis
Ref Expression
con3i.a
Assertion
Ref Expression
con3i

Proof of Theorem con3i
StepHypRef Expression
1 id 22 . 2
2 con3i.a . 2
31, 2nsyl 121 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4
This theorem is referenced by:  pm2.51  153  pm2.65i  173  pm5.21ni  352  pm2.45  397  pm2.46  398  nbiorOLD  861  pm5.14  886  con3th  958  rb-ax2  1586  rb-ax4  1588  stoic1a  1605  ax13  2047  sbequi  2116  ax13fromc9  2235  axc711  2244  axc711toc7  2246  axc5c711toc7  2250  equidqe  2252  equidq  2254  ax12indalem  2275  euor2  2333  baroco  2405  necon3bi  2686  necon1biOLD  2691  eueq3  3274  sbc2or  3336  sbcimdv  3396  sbcrext  3410  difrab  3771  abvor0  3803  csbprc  3821  sbcel12  3823  sbcne12  3827  sbcel2  3831  ifeqor  3985  ifan  3987  nelpri  4050  nelprd  4051  opprc1  4240  opprc2  4241  sbcbr123  4503  snexALT  4638  mosubopt  4750  csbopab  4784  csbxp  5086  soirri  5398  soirriOLD  5403  csbiota  5585  nfvres  5901  fvco4i  5951  fvmptex  5966  fvopab4ndm  5978  ressnop0  6078  csbriota  6269  ovprc  6326  ovprc1  6327  ovprc2  6328  ndmovass  6463  ndmovdistr  6464  eldifpw  6612  nlimsucg  6677  tfindsg  6695  findsg  6727  curry1val  6893  curry2val  6897  extmptsuppeq  6943  funsssuppss  6945  eceqoveq  7435  fiprc  7617  sdomirr  7674  domtriord  7683  2pwuninel  7692  mapdom1  7702  nfielex  7768  relprcnfsupp  7852  supval2  7935  wemapso2  8000  card2inf  8002  en2lp  8051  wemapwe  8160  wemapweOLD  8161  rankxplim3  8320  fidomtri2  8396  alephnbtwn  8473  kmlem2  8552  isfin7-2  8797  dominf  8846  ac6n  8886  alephval2  8968  dominfac  8969  axpowndlem3  8996  gchdomtri  9028  nlt1pi  9305  adderpq  9355  mulerpq  9356  zeo  10973  fzoval  11830  bcpasc  12399  hashnemnf  12417  hasheq0  12433  hashunx  12454  hashbc  12502  prmreclem4  14437  ressinbas  14693  natfval  15315  fucbas  15329  fuchom  15330  homarcl  15355  arwval  15370  coafval  15391  grpidval  15887  symgbas  16405  efgval  16735  gsum2dlem1  16997  gsum2dlem2  16998  gsum2dOLD  17000  dprddomprc  17031  dprdval0prc  17033  psrvscafval  18043  mavmul0g  19055  mdetralt  19110  mdetunilem9  19122  tgdif0  19494  resstopn  19687  cfinfil  20394  pcofval  21510  i1fima2  22086  i1fd  22088  itgeq2  22184  ibladdlem  22226  cusgrafi  24482  uvtx01vtx  24492  frgra2v  24999  2spotiundisj  25062  numclwwlkdisj  25080  avril1  25171  nmobndseqi  25694  nonbooli  26569  chpssati  27282  xrge0neqmnf  27679  hasheuni  28091  ddemeas  28208  rdgprc0  29226  distel  29236  predpoirr  29277  predfrirr  29278  linedegen  29793  ordcmp  29912  wl-naev  29982  wl-ax11-lem8  30032  cnambfre  30063  itg2addnclem3  30068  ibladdnclem  30071  frinfm  30226  tsbi3  30542  jm2.22  30937  nanorxor  31185  binomcxplemfrat  31256  binomcxplemradcnv  31257  pm10.251  31265  axc5c4c711toc7  31311  fzdifsuc2  31512  infrglb  31584  cncfiooicc  31697  itgcoscmulx  31768  ndmafv  32225  nfunsnafv  32227  afvprc  32229  afvnufveq  32232  aovprc  32273  ndmaovass  32291  ndmaovdistr  32292  en3lpVD  33645  ax6e2ndeqVD  33709  2sb5ndVD  33710  ax6e2ndeqALT  33731  2sb5ndALT  33732  sineq0ALT  33737  bnj1143  33849  bj-con3thALT  34162  bj-babygodel  34191  bj-nexrt  34245  bj-csbprc  34476  bj-projval  34554  hdmap1eulem  37551  hdmapevec  37565  rp-fakeimass  37736
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
  Copyright terms: Public domain W3C validator