Theorem con3i 154

Description: A contraposition inference. Inference associated with con3 153. Its associated inference is mto 196. (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 140	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:  conax1  170  pm2.65i  193  pm5.21ni  379  pm2.45  879  pm2.46  880  con3ALT  1084  rb-ax2  1756  rb-ax4  1758  emptyex  1911  naev  2064  ax13ALT  2426  barocoALT  2679  necon3bi  2971  prcnel  3456  sbc2or  3726  difrab  4243  sbcel12  4343  sbcne12  4347  sbcel2  4350  rexn0  4442  ifeqor  4511  ifan  4513  nelpri  4591  nelprd  4593  eqoreldif  4621  snexALT  5307  csbopab  5469  nprrel12  5646  csbxp  5687  soirri  6036  predpoirr  6240  predfrirr  6241  nsuceq0  6350  csbiota  6430  eldifpw  7627  nlimsucg  7698  tfindsg  7716  findsg  7755  curry1val  7954  curry2val  7958  fsetdmprc0  8652  fiprc  8844  sdomirr  8910  domtriord  8919  2pwuninel  8928  mapdom1  8938  nfielex  9056  relprcnfsupp  9140  wemapso2  9321  card2inf  9323  en2lp  9373  wemapwe  9464  rankxplim3  9648  fidomtri2  9761  alephnbtwn  9836  kmlem2  9916  isfin7-2  10161  dominf  10210  ac6n  10250  alephval2  10337  dominfac  10338  gchdomtri  10394  nlt1pi  10671  zeo  12415  bcpasc  14044  hashnemnf  14067  hasheq0  14087  hashunx  14110  hashbc  14174  pfxval0  14398  flodddiv4lt  16133  prmreclem4  16629  ressinbas  16964  natfval  17671  fucbas  17686  fuchom  17687  fuchomOLD  17688  coafval  17788  efgval  19332  gsum2dlem1  19580  gsum2dlem2  19581  dprddomprc  19612  dprdval0prc  19614  psrvscafval  21168  mavmul0g  21711  mdetralt  21766  mdetunilem9  21778  cfinfil  23053  pcofval  24182  i1fima2  24852  i1fd  24854  itgeq2  24951  ibladdlem  24993  nbgrnself2  27736  clwwlknondisj  28484  nfrgr2v  28645  avril1  28836  nmobndseqi  29150  nonbooli  30022  chpssati  30734  hashxpe  31136  hasheuni  32062  ddemeas  32213  bnj1143  32779  distel  33788  linedegen  34454  ordcmp  34645  bj-babygodel  34794  bj-nexrt  34883  bj-csbprc  35104  onsucuni3  35547  finxpnom  35581  wl-ifp-ncond1  35644  wl-ax11-lem8  35752  unccur  35769  matunitlindflem1  35782  poimirlem26  35812  poimirlem27  35813  poimirlem31  35817  cnambfre  35834  ibladdnclem  35842  frinfm  35902  tsbi3  36302  ax13fromc9  36927  axc711  36935  axc711toc7  36937  axc5c711toc7  36941  equidqe  36943  equidq  36945  ax12indalem  36966  hdmap1eulem  39843  hdmapevec  39856  jm2.22  40824  clsk1indlem2  41659  nanorxor  41930  binomcxplemfrat  41976  binomcxplemradcnv  41977  pm10.251  41985  axc5c4c711toc7  42029  en3lpVD  42472  ax6e2ndeqVD  42536  2sb5ndVD  42537  ax6e2ndeqALT  42558  2sb5ndALT  42559  sineq0ALT  42564  nel1nelin  42702  nel2nelin  42703  axccdom  42769  fzdifsuc2  42856  liminf0  43341  cncfiooicc  43442  itgcoscmulx  43517  sge0sn  43924  isomenndlem  44075  hoidmvlelem2  44141  nabctnabc  44437  dfafv2  44635  afv2ndefb  44727  spr0el  44945  prmdvdsfmtnof1lem2  45048  et-ltneverrefl  46521  singoutnword  46528