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

Theorem con3i 149
Description: A contraposition inference. Inference associated with con3 148. Its associated inference is mto 187. (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 134 1 𝜓 → ¬ 𝜑)
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  164  pm2.65i  184  pm5.21ni  366  pm2.45  411  pm2.46  412  pm5.14  926  con3ALT  1026  con3OLD  1029  rb-ax2  1669  rb-ax4  1671  ax13OLD  2293  sbequi  2363  euor2  2502  baroco  2560  necon3bi  2808  prcnel  3191  eueq3  3348  sbc2or  3411  sbcimdvOLD  3466  sbcrextOLD  3479  difrab  3860  csbprcOLD  3933  sbcel12  3935  sbcne12  3938  sbcel2  3941  ifeqor  4082  ifan  4084  nelpri  4149  nelprd  4151  eqoreldif  4172  opprc1  4358  opprc2  4359  snexALT  4773  mosubopt  4888  csbopab  4922  csbxp  5113  soirri  5428  predpoirr  5611  predfrirr  5612  nsuceq0  5708  csbiota  5783  nfvres  6119  fvco4i  6171  fvmptex  6188  fvopab4ndm  6200  ressnop0  6303  csbriota  6501  ovprc  6559  ovprc1  6560  ovprc2  6561  ndmovass  6698  ndmovdistr  6699  eldifpw  6846  nlimsucg  6912  tfindsg  6930  findsg  6963  curry1val  7135  curry2val  7139  extmptsuppeq  7184  funsssuppss  7186  eceqoveq  7718  fiprc  7902  sdomirr  7960  domtriord  7969  2pwuninel  7978  mapdom1  7988  nfielex  8052  relprcnfsupp  8139  supval2  8222  wemapso2  8319  card2inf  8321  en2lp  8371  wemapwe  8455  rankxplim3  8605  fidomtri2  8681  alephnbtwn  8755  kmlem2  8834  isfin7-2  9079  dominf  9128  ac6n  9168  alephval2  9251  dominfac  9252  axpowndlem3  9278  gchdomtri  9308  nlt1pi  9585  adderpq  9635  mulerpq  9636  zeo  11298  xrge0neqmnf  12106  fzoval  12298  bcpasc  12928  hashnemnf  12949  hasheq0  12970  hashunx  12991  hashbc  13049  flodddiv4lt  14926  prmreclem4  15410  ressinbas  15712  natfval  16378  fucbas  16392  fuchom  16393  arwval  16465  coafval  16486  grpidval  17032  symgbas  17572  efgval  17902  gsum2dlem1  18141  gsum2dlem2  18142  dprddomprc  18171  dprdval0prc  18173  psrvscafval  19160  mavmul0g  20126  mdetralt  20181  mdetunilem9  20193  tgdif0  20555  resstopn  20748  cfinfil  21455  pcofval  22566  i1fima2  23197  i1fd  23199  itgeq2  23295  ibladdlem  23337  cusgrafi  25804  uvtx01vtx  25814  frgra2v  26320  2spotiundisj  26383  numclwwlkdisj  26401  avril1  26505  nmobndseqi  26812  nonbooli  27688  chpssati  28400  hasheuni  29268  inelpisys  29338  ddemeas  29420  bnj1143  29909  rdgprc0  30737  distel  30747  linedegen  31214  ordcmp  31410  bj-babygodel  31555  bj-nexrt  31663  bj-csbprc  31890  bj-projval  31971  onsucuni3  32185  finxpnom  32208  wl-naev  32275  wl-hbnaev  32278  wl-ax11-lem8  32342  unccur  32356  matunitlindflem1  32369  poimirlem26  32399  poimirlem27  32400  poimirlem31  32404  cnambfre  32422  itg2addnclem3  32427  ibladdnclem  32430  frinfm  32494  tsbi3  32906  ax13fromc9  33003  axc711  33011  axc711toc7  33013  axc5c711toc7  33017  equidqe  33019  equidq  33021  ax12indalem  33042  hdmap1eulem  35925  hdmapevec  35939  jm2.22  36374  rp-fakeimass  36670  or3or  37133  clsk1indlem2  37154  nanorxor  37320  binomcxplemfrat  37366  binomcxplemradcnv  37367  pm10.251  37375  axc5c4c711toc7  37421  en3lpVD  37896  ax6e2ndeqVD  37961  2sb5ndVD  37962  ax6e2ndeqALT  37983  2sb5ndALT  37984  sineq0ALT  37989  axccdom  38205  fzdifsuc2  38260  cncfiooicc  38574  itgcoscmulx  38655  sge0sn  39066  iundjiunlem  39146  isomenndlem  39214  hoidmvlelem2  39280  smfmbfcex  39440  nabctnabc  39541  ndmafv  39664  nfunsnafv  39666  afvprc  39668  afvnufveq  39671  aovprc  39712  ndmaovass  39730  ndmaovdistr  39731  prmdvdsfmtnof1lem2  39830  clwwlksndisj  41272  nfrgr2v  41434
  Copyright terms: Public domain W3C validator