Theorem con3i 155

Description: A contraposition inference. Inference associated with con3 154. 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

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  conax1  171  pm2.65iOLD  197  pm5.21ni  380  pm2.45  895  pm2.46  896  con3ALT  1101  rb-ax2  1785  rb-ax4  1787  emptyex  1939  excomimw  2076  naev  2094  ax13ALT  2454  barocoALT  2701  necon3bi  2981  prcnel  3475  sbc2or  3747  nel1nelin  4103  nel2nelin  4104  difrab  4262  sbcel12  4368  sbcne12  4372  sbcel2  4375  rexn0  4451  ifeqor  4533  ifan  4535  nelpri  4612  nelprd  4614  eqoreldif  4642  vneqv  5269  snexALT  5344  csbopab  5529  nprrel12  5708  csbxp  5752  soirri  6121  predpoirr  6338  predfrirr  6339  nsuceq0  6450  csbiota  6534  eldifpw  7784  nlimsucg  7855  tfindsg  7874  findsg  7911  curry1val  8120  curry2val  8124  fsetdmprc0  8882  fiprc  9077  sdomirr  9138  domtriord  9147  2pwuninel  9156  mapdom1  9166  nfielex  9270  relprcnfsupp  9361  wemapso2  9552  card2inf  9554  en2lp  9612  wemapwe  9703  rankxplim3  9903  fidomtri2  10080  alephnbtwn  10155  kmlem2  10235  isfin7-2  10479  dominf  10528  ac6n  10568  alephval2  10662  dominfac  10663  gchdomtri  10719  nlt1pi  10996  indval0  12329  zeo  12790  bcpasc  14470  hashnemnf  14493  hasheq0  14512  hashunx  14535  hashbc  14603  pfxval0  14832  flodddiv4lt  16594  prmreclem4  17104  ressinbas  17430  natfval  18131  fucbas  18145  fuchom  18146  coafval  18246  efgval  19938  gsum2dlem1  20191  gsum2dlem2  20192  dprddomprc  20223  dprdval0prc  20225  isfieldidl  21547  psrvscafval  22263  mavmul0g  22875  mdetralt  22930  mdetunilem9  22942  matunitlindflem1  23001  cfinfil  24219  pcofval  25338  i1fima2  26007  i1fd  26009  itgeq2  26105  ibladdlem  26147  nbgrnself2  29948  clwwlknondisj  30709  nfrgr2v  30880  avril1  31071  nmobndseqi  31388  nonbooli  32260  chpssati  32972  nn0difffzod  33444  hashxpe  33447  gsumfs2d  33670  1arithufdlem4  34127  hasheuni  34765  ddemeas  34917  bnj1143  35468  rmo6  35758  fineqvnttrclse  35850  fineqvinfep  35851  kardval  35878  kard0b  35885  distel  36659  linedegen  37002  ordcmp  37329  bj-babygodel  37567  bj-nexrt  37688  bj-csbprc  37916  onsucuni3  38397  finxpnom  38431  wl-ifp-ncond1  38494  unccur  38633  poimirlem26  38671  poimirlem27  38672  poimirlem31  38676  cnambfre  38693  ibladdnclem  38701  frinfm  38776  tsbi3  39174  mopickr  39410  ax13fromc9  40070  axc711  40078  axc711toc7  40080  axc5c711toc7  40084  equidqe  40086  equidq  40088  ax12indalem  40109  hdmap1eulem  42986  hdmapevec  42999  intnanrt  43365  jm2.22  44109  clsk1indlem2  45149  nanorxor  45396  binomcxplemfrat  45442  binomcxplemradcnv  45443  pm10.251  45451  axc5c4c711toc7  45495  en3lpVD  45934  ax6e2ndeqVD  45998  2sb5ndVD  45999  ax6e2ndeqALT  46020  2sb5ndALT  46021  sineq0ALT  46026  axccdom  46342  fzdifsuc2  46433  liminf0  46910  cncfiooicc  47011  itgcoscmulx  47086  sge0sn  47496  isomenndlem  47647  hoidmvlelem2  47713  et-ltneverrefl  47988  quantgodelALT  47992  nabctnabc  48108  dfafv2  48309  afv2ndefb  48401  spr0el  48671  prmdvdsfmtnof1lem2  48777  fucofvalne  50554