Theorem con3i 150

Description: A contraposition inference. Inference associated with con3 149. Its associated inference is mto 188. (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

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (¬ 𝜓 → ¬ 𝜓)
2		con3i.a	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	nsyl 135	1 ⊢ (¬ 𝜓 → ¬ 𝜑)

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  165  pm2.65i  185  pm5.21ni  367  pm2.45  412  pm2.46  413  pm5.14  930  con3ALT  1032  con3OLD  1035  rb-ax2  1678  rb-ax4  1680  ax13ALT  2305  sbequi  2375  euor2  2514  baroco  2572  necon3bi  2820  prcnel  3218  eueq3  3381  sbc2or  3444  sbcimdvOLD  3499  sbcrextOLD  3512  difrab  3901  csbprcOLD  3981  sbcel12  3983  sbcne12  3986  sbcel2  3989  ifeqor  4132  ifan  4134  nelpri  4201  nelprd  4203  eqoreldif  4225  opprc1  4425  opprc2  4426  snexALT  4852  mosubopt  4972  csbopab  5008  nprrel12  5160  csbxp  5200  soirri  5522  predpoirr  5708  predfrirr  5709  nsuceq0  5805  csbiota  5881  nfvres  6224  fvco4i  6276  fvmptex  6294  fvopab4ndm  6307  ressnop0  6420  csbriota  6623  ovprc  6683  ovprc1  6684  ovprc2  6685  ndmovass  6822  ndmovdistr  6823  eldifpw  6976  nlimsucg  7042  tfindsg  7060  findsg  7093  curry1val  7270  curry2val  7274  extmptsuppeq  7319  funsssuppss  7321  eceqoveq  7853  fiprc  8039  sdomirr  8097  domtriord  8106  2pwuninel  8115  mapdom1  8125  nfielex  8189  relprcnfsupp  8278  supval2  8361  wemapso2  8458  card2inf  8460  en2lp  8510  wemapwe  8594  rankxplim3  8744  fidomtri2  8820  alephnbtwn  8894  kmlem2  8973  isfin7-2  9218  dominf  9267  ac6n  9307  alephval2  9394  dominfac  9395  axpowndlem3  9421  gchdomtri  9451  nlt1pi  9728  adderpq  9778  mulerpq  9779  zeo  11463  xrge0neqmnf  12276  fzoval  12471  bcpasc  13108  hashnemnf  13132  hasheq0  13154  hashunx  13175  hashbc  13237  flodddiv4lt  15139  prmreclem4  15623  ressinbas  15936  natfval  16606  fucbas  16620  fuchom  16621  arwval  16693  coafval  16714  grpidval  17260  symgbas  17800  efgval  18130  gsum2dlem1  18369  gsum2dlem2  18370  dprddomprc  18399  dprdval0prc  18401  psrvscafval  19390  mavmul0g  20359  mdetralt  20414  mdetunilem9  20426  tgdif0  20796  resstopn  20990  cfinfil  21697  pcofval  22810  i1fima2  23446  i1fd  23448  itgeq2  23544  ibladdlem  23586  clwwlksndisj  26973  nfrgr2v  27136  avril1  27319  nmobndseqi  27634  nonbooli  28510  chpssati  29222  hasheuni  30147  inelpisys  30217  ddemeas  30299  bnj1143  30861  rdgprc0  31699  distel  31709  linedegen  32250  ordcmp  32446  bj-babygodel  32588  bj-nexrt  32682  bj-csbprc  32904  bj-projval  32984  onsucuni3  33215  finxpnom  33238  wl-naev  33302  wl-hbnaev  33305  wl-ax11-lem8  33369  unccur  33392  matunitlindflem1  33405  poimirlem26  33435  poimirlem27  33436  poimirlem31  33440  cnambfre  33458  itg2addnclem3  33463  ibladdnclem  33466  frinfm  33530  tsbi3  33942  ax13fromc9  34191  axc711  34199  axc711toc7  34201  axc5c711toc7  34205  equidqe  34207  equidq  34209  ax12indalem  34230  hdmap1eulem  37113  hdmapevec  37127  jm2.22  37562  rp-fakeimass  37857  or3or  38319  clsk1indlem2  38340  nanorxor  38504  binomcxplemfrat  38550  binomcxplemradcnv  38551  pm10.251  38559  axc5c4c711toc7  38605  en3lpVD  39080  ax6e2ndeqVD  39145  2sb5ndVD  39146  ax6e2ndeqALT  39167  2sb5ndALT  39168  sineq0ALT  39173  nel1nelin  39337  nel2nelin  39338  axccdom  39416  fzdifsuc2  39525  liminf0  40025  cncfiooicc  40107  itgcoscmulx  40185  sge0sn  40596  iundjiunlem  40676  isomenndlem  40744  hoidmvlelem2  40810  smfmbfcex  40968  nabctnabc  41098  ndmafv  41220  nfunsnafv  41222  afvnufveq  41227  aovprc  41268  ndmaovass  41286  ndmaovdistr  41287  prmdvdsfmtnof1lem2  41497  spr0el  41732  setrec2lem1  42440