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  881  pm2.46  882  con3ALT  1086  rb-ax2  1756  rb-ax4  1758  emptyex  1911  naev  2064  ax13ALT  2425  barocoALT  2673  necon3bi  2968  prcnel  3498  sbc2or  3785  difrab  4307  sbcel12  4407  sbcne12  4411  sbcel2  4414  rexn0  4509  ifeqor  4578  ifan  4580  nelpri  4656  nelprd  4658  eqoreldif  4687  snexALT  5380  csbopab  5554  nprrel12  5732  csbxp  5773  soirri  6124  predpoirr  6331  predfrirr  6332  nsuceq0  6444  csbiota  6533  eldifpw  7750  nlimsucg  7826  tfindsg  7845  findsg  7885  curry1val  8086  curry2val  8090  fsetdmprc0  8845  fiprc  9041  sdomirr  9110  domtriord  9119  2pwuninel  9128  mapdom1  9138  nfielex  9269  relprcnfsupp  9360  wemapso2  9544  card2inf  9546  en2lp  9597  wemapwe  9688  rankxplim3  9872  fidomtri2  9985  alephnbtwn  10062  kmlem2  10142  isfin7-2  10387  dominf  10436  ac6n  10476  alephval2  10563  dominfac  10564  gchdomtri  10620  nlt1pi  10897  zeo  12644  bcpasc  14277  hashnemnf  14300  hasheq0  14319  hashunx  14342  hashbc  14408  pfxval0  14622  flodddiv4lt  16354  prmreclem4  16848  ressinbas  17186  natfval  17893  fucbas  17908  fuchom  17909  fuchomOLD  17910  coafval  18010  efgval  19578  gsum2dlem1  19830  gsum2dlem2  19831  dprddomprc  19862  dprdval0prc  19864  psrvscafval  21491  mavmul0g  22037  mdetralt  22092  mdetunilem9  22104  cfinfil  23379  pcofval  24508  i1fima2  25178  i1fd  25180  itgeq2  25277  ibladdlem  25319  nbgrnself2  28597  clwwlknondisj  29344  nfrgr2v  29505  avril1  29696  nmobndseqi  30010  nonbooli  30882  chpssati  31594  nn0difffzod  31994  hashxpe  31997  hasheuni  33021  ddemeas  33172  bnj1143  33739  distel  34713  linedegen  35053  ordcmp  35270  bj-babygodel  35419  bj-nexrt  35508  bj-csbprc  35728  onsucuni3  36186  finxpnom  36220  wl-ifp-ncond1  36283  wl-ax11-lem8  36392  unccur  36409  matunitlindflem1  36422  poimirlem26  36452  poimirlem27  36453  poimirlem31  36457  cnambfre  36474  ibladdnclem  36482  frinfm  36541  tsbi3  36941  mopickr  37170  ax13fromc9  37714  axc711  37722  axc711toc7  37724  axc5c711toc7  37728  equidqe  37730  equidq  37732  ax12indalem  37753  hdmap1eulem  40631  hdmapevec  40644  jm2.22  41667  clsk1indlem2  42726  nanorxor  42997  binomcxplemfrat  43043  binomcxplemradcnv  43044  pm10.251  43052  axc5c4c711toc7  43096  en3lpVD  43539  ax6e2ndeqVD  43603  2sb5ndVD  43604  ax6e2ndeqALT  43625  2sb5ndALT  43626  sineq0ALT  43631  nel1nelin  43768  nel2nelin  43769  axccdom  43854  fzdifsuc2  43955  liminf0  44444  cncfiooicc  44545  itgcoscmulx  44620  sge0sn  45030  isomenndlem  45181  hoidmvlelem2  45247  et-ltneverrefl  45522  singoutnword  45531  nabctnabc  45576  dfafv2  45775  afv2ndefb  45867  spr0el  46085  prmdvdsfmtnof1lem2  46188