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 ⊢ (¬ 𝜓 → ¬ 𝜑)

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  171  pm2.65iOLD  197  pm5.21ni  380  pm2.45  894  pm2.46  895  con3ALT  1101  rb-ax2  1783  rb-ax4  1785  emptyex  1937  excomimw  2074  naev  2092  ax13ALT  2457  barocoALT  2704  necon3bi  2984  prcnel  3480  sbc2or  3753  nel1nelin  4160  nel2nelin  4161  difrab  4271  sbcel12  4376  sbcne12  4380  sbcel2  4383  rexn0  4457  ifeqor  4539  ifan  4541  nelpri  4621  nelprd  4623  eqoreldif  4651  vneqv  5279  snexALT  5354  csbopab  5540  nprrel12  5719  csbxp  5762  soirri  6126  predpoirr  6334  predfrirr  6335  nsuceq0  6446  csbiota  6529  eldifpw  7763  nlimsucg  7834  tfindsg  7853  findsg  7890  curry1val  8096  curry2val  8100  fsetdmprc0  8848  fiprc  9037  sdomirr  9098  domtriord  9107  2pwuninel  9116  mapdom1  9126  nfielex  9230  relprcnfsupp  9320  wemapso2  9511  card2inf  9513  en2lp  9571  wemapwe  9662  rankxplim3  9849  fidomtri2  9976  alephnbtwn  10051  kmlem2  10131  isfin7-2  10375  dominf  10424  ac6n  10464  alephval2  10552  dominfac  10553  gchdomtri  10609  nlt1pi  10886  indval0  12217  zeo  12677  bcpasc  14353  hashnemnf  14376  hasheq0  14395  hashunx  14418  hashbc  14486  pfxval0  14710  flodddiv4lt  16470  prmreclem4  16974  ressinbas  17300  natfval  18001  fucbas  18015  fuchom  18016  coafval  18116  efgval  19782  gsum2dlem1  20035  gsum2dlem2  20036  dprddomprc  20067  dprdval0prc  20069  isfieldidl  21386  psrvscafval  22098  mavmul0g  22710  mdetralt  22765  mdetunilem9  22777  cfinfil  24050  pcofval  25169  i1fima2  25838  i1fd  25840  itgeq2  25937  ibladdlem  25979  nbgrnself2  29710  clwwlknondisj  30462  nfrgr2v  30623  avril1  30814  nmobndseqi  31131  nonbooli  32003  chpssati  32715  nn0difffzod  33149  hashxpe  33152  gsumfs2d  33381  1arithufdlem4  33837  hasheuni  34475  ddemeas  34626  bnj1143  35178  fineqvnttrclse  35537  fineqvinfep  35538  kardval  35565  kard0b  35572  distel  36293  linedegen  36635  ordcmp  36958  bj-babygodel  37196  bj-nexrt  37317  bj-csbprc  37545  onsucuni3  38013  finxpnom  38047  wl-ifp-ncond1  38110  unccur  38254  matunitlindflem1  38267  poimirlem26  38297  poimirlem27  38298  poimirlem31  38302  cnambfre  38319  ibladdnclem  38327  frinfm  38386  tsbi3  38784  mopickr  39020  ax13fromc9  39680  axc711  39688  axc711toc7  39690  axc5c711toc7  39694  equidqe  39696  equidq  39698  ax12indalem  39719  hdmap1eulem  42596  hdmapevec  42609  intnanrt  42975  jm2.22  43722  clsk1indlem2  44768  nanorxor  45015  binomcxplemfrat  45061  binomcxplemradcnv  45062  pm10.251  45070  axc5c4c711toc7  45114  en3lpVD  45553  ax6e2ndeqVD  45617  2sb5ndVD  45618  ax6e2ndeqALT  45639  2sb5ndALT  45640  sineq0ALT  45645  axccdom  45938  fzdifsuc2  46029  liminf0  46507  cncfiooicc  46608  itgcoscmulx  46683  sge0sn  47093  isomenndlem  47244  hoidmvlelem2  47310  et-ltneverrefl  47585  quantgodelALT  47589  nabctnabc  47668  dfafv2  47869  afv2ndefb  47961  spr0el  48231  prmdvdsfmtnof1lem2  48337  fucofvalne  50103