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

Theorem con3i 157
Description: A contraposition inference. Inference associated with con3 156. Its associated inference is mto 200. (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 142 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:  conax1  173  pm2.65i  197  pm5.21ni  382  pm2.45  879  pm2.46  880  con3ALT  1082  rb-ax2  1755  rb-ax4  1757  emptyex  1908  naev  2065  ax13ALT  2448  sbequiOLD  2534  sbequiALT  2596  barocoALT  2763  necon3bi  3037  prcnel  3493  sbc2or  3756  difrab  4251  sbcel12  4332  sbcne12  4336  sbcel2  4339  ifeqor  4488  ifan  4490  nelpri  4568  nelprd  4570  eqoreldif  4596  snexALT  5261  csbopab  5419  nprrel12  5587  csbxp  5627  soirri  5964  predpoirr  6154  predfrirr  6155  nsuceq0  6249  csbiota  6327  eldifpw  7475  nlimsucg  7542  tfindsg  7560  findsg  7595  curry1val  7787  curry2val  7791  fiprc  8582  sdomirr  8642  domtriord  8651  2pwuninel  8660  mapdom1  8670  nfielex  8735  relprcnfsupp  8824  wemapso2  9005  card2inf  9007  en2lp  9057  wemapwe  9148  rankxplim3  9298  fidomtri2  9411  alephnbtwn  9486  kmlem2  9566  isfin7-2  9807  dominf  9856  ac6n  9896  alephval2  9983  dominfac  9984  gchdomtri  10040  nlt1pi  10317  zeo  12056  bcpasc  13677  hashnemnf  13700  hasheq0  13720  hashunx  13743  hashbc  13807  pfxval0  14029  flodddiv4lt  15755  prmreclem4  16244  ressinbas  16551  natfval  17207  fucbas  17221  fuchom  17222  coafval  17315  efgval  18834  gsum2dlem1  19081  gsum2dlem2  19082  dprddomprc  19113  dprdval0prc  19115  psrvscafval  20626  mavmul0g  21156  mdetralt  21211  mdetunilem9  21223  cfinfil  22496  pcofval  23613  i1fima2  24281  i1fd  24283  itgeq2  24379  ibladdlem  24421  nbgrnself2  27148  clwwlknondisj  27894  nfrgr2v  28055  avril1  28246  nmobndseqi  28560  nonbooli  29432  chpssati  30144  hashxpe  30539  hasheuni  31418  ddemeas  31569  bnj1143  32136  distel  33122  linedegen  33678  ordcmp  33869  bj-babygodel  34011  bj-nexrt  34100  bj-csbprc  34311  onsucuni3  34745  finxpnom  34779  wl-ax11-lem8  34951  unccur  35002  matunitlindflem1  35015  poimirlem26  35045  poimirlem27  35046  poimirlem31  35050  cnambfre  35067  ibladdnclem  35075  frinfm  35135  tsbi3  35535  ax13fromc9  36164  axc711  36172  axc711toc7  36174  axc5c711toc7  36178  equidqe  36180  equidq  36182  ax12indalem  36203  hdmap1eulem  39080  hdmapevec  39093  jm2.22  39870  clsk1indlem2  40682  nanorxor  40947  binomcxplemfrat  40993  binomcxplemradcnv  40994  pm10.251  41002  axc5c4c711toc7  41046  en3lpVD  41489  ax6e2ndeqVD  41553  2sb5ndVD  41554  ax6e2ndeqALT  41575  2sb5ndALT  41576  sineq0ALT  41581  nel1nelin  41724  nel2nelin  41725  axccdom  41795  fzdifsuc2  41885  liminf0  42378  cncfiooicc  42479  itgcoscmulx  42554  sge0sn  42961  isomenndlem  43112  hoidmvlelem2  43178  nabctnabc  43467  dfafv2  43631  afv2ndefb  43723  spr0el  43942  prmdvdsfmtnof1lem2  44045
  Copyright terms: Public domain W3C validator