Theorem con3i 154

Description: A contraposition inference. Inference associated with con3 153. Its associated inference is mto 197. (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  194  pm5.21ni  377  pm2.45  881  pm2.46  882  con3ALT  1084  rb-ax2  1754  rb-ax4  1756  emptyex  1908  excomimw  2045  naev  2063  ax13ALT  2427  barocoALT  2674  necon3bi  2955  prcnel  3463  sbc2or  3746  nel1nelin  4156  nel2nelin  4157  difrab  4267  sbcel12  4360  sbcne12  4364  sbcel2  4367  rexn0  4446  ifeqor  4528  ifan  4530  nelpri  4609  nelprd  4611  eqoreldif  4639  snexALT  5325  csbopab  5500  nprrel12  5679  csbxp  5722  soirri  6080  predpoirr  6288  predfrirr  6289  nsuceq0  6399  csbiota  6482  eldifpw  7710  nlimsucg  7781  tfindsg  7800  findsg  7836  curry1val  8044  curry2val  8048  fsetdmprc0  8788  fiprc  8977  sdomirr  9038  domtriord  9047  2pwuninel  9056  mapdom1  9066  nfielex  9169  relprcnfsupp  9259  wemapso2  9450  card2inf  9452  en2lp  9507  wemapwe  9598  rankxplim3  9785  fidomtri2  9898  alephnbtwn  9973  kmlem2  10054  isfin7-2  10298  dominf  10347  ac6n  10387  alephval2  10474  dominfac  10475  gchdomtri  10531  nlt1pi  10808  zeo  12569  bcpasc  14235  hashnemnf  14258  hasheq0  14277  hashunx  14300  hashbc  14367  pfxval0  14591  flodddiv4lt  16335  prmreclem4  16838  ressinbas  17163  natfval  17864  fucbas  17878  fuchom  17879  coafval  17979  efgval  19637  gsum2dlem1  19890  gsum2dlem2  19891  dprddomprc  19922  dprdval0prc  19924  psrvscafval  21895  mavmul0g  22488  mdetralt  22543  mdetunilem9  22555  cfinfil  23828  pcofval  24957  i1fima2  25627  i1fd  25629  itgeq2  25726  ibladdlem  25768  nbgrnself2  29359  clwwlknondisj  30112  nfrgr2v  30273  avril1  30464  nmobndseqi  30780  nonbooli  31652  chpssati  32364  nn0difffzod  32812  hashxpe  32815  gsumfs2d  33072  1arithufdlem4  33556  hasheuni  34170  ddemeas  34321  bnj1143  34874  fineqvnttrclse  35216  distel  35917  linedegen  36259  ordcmp  36563  bj-babygodel  36719  bj-nexrt  36809  bj-csbprc  37027  onsucuni3  37484  finxpnom  37518  wl-ifp-ncond1  37581  unccur  37716  matunitlindflem1  37729  poimirlem26  37759  poimirlem27  37760  poimirlem31  37764  cnambfre  37781  ibladdnclem  37789  frinfm  37848  tsbi3  38248  mopickr  38468  ax13fromc9  39078  axc711  39086  axc711toc7  39088  axc5c711toc7  39092  equidqe  39094  equidq  39096  ax12indalem  39117  hdmap1eulem  41994  hdmapevec  42007  intnanrt  42372  jm2.22  43152  clsk1indlem2  44199  nanorxor  44462  binomcxplemfrat  44508  binomcxplemradcnv  44509  pm10.251  44517  axc5c4c711toc7  44561  en3lpVD  45001  ax6e2ndeqVD  45065  2sb5ndVD  45066  ax6e2ndeqALT  45087  2sb5ndALT  45088  sineq0ALT  45093  axccdom  45382  fzdifsuc2  45474  liminf0  45953  cncfiooicc  46054  itgcoscmulx  46129  sge0sn  46539  isomenndlem  46690  hoidmvlelem2  46756  et-ltneverrefl  47031  nabctnabc  47093  dfafv2  47294  afv2ndefb  47386  spr0el  47644  prmdvdsfmtnof1lem2  47747  fucofvalne  49486