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  3787  difrab  4309  sbcel12  4409  sbcne12  4413  sbcel2  4416  rexn0  4511  ifeqor  4580  ifan  4582  nelpri  4658  nelprd  4660  eqoreldif  4689  snexALT  5382  csbopab  5556  nprrel12  5735  csbxp  5776  soirri  6128  predpoirr  6335  predfrirr  6336  nsuceq0  6448  csbiota  6537  eldifpw  7755  nlimsucg  7831  tfindsg  7850  findsg  7890  curry1val  8091  curry2val  8095  fsetdmprc0  8849  fiprc  9045  sdomirr  9114  domtriord  9123  2pwuninel  9132  mapdom1  9142  nfielex  9273  relprcnfsupp  9364  wemapso2  9548  card2inf  9550  en2lp  9601  wemapwe  9692  rankxplim3  9876  fidomtri2  9989  alephnbtwn  10066  kmlem2  10146  isfin7-2  10391  dominf  10440  ac6n  10480  alephval2  10567  dominfac  10568  gchdomtri  10624  nlt1pi  10901  zeo  12648  bcpasc  14281  hashnemnf  14304  hasheq0  14323  hashunx  14346  hashbc  14412  pfxval0  14626  flodddiv4lt  16358  prmreclem4  16852  ressinbas  17190  natfval  17897  fucbas  17912  fuchom  17913  fuchomOLD  17914  coafval  18014  efgval  19585  gsum2dlem1  19838  gsum2dlem2  19839  dprddomprc  19870  dprdval0prc  19872  psrvscafval  21509  mavmul0g  22055  mdetralt  22110  mdetunilem9  22122  cfinfil  23397  pcofval  24526  i1fima2  25196  i1fd  25198  itgeq2  25295  ibladdlem  25337  nbgrnself2  28617  clwwlknondisj  29364  nfrgr2v  29525  avril1  29716  nmobndseqi  30032  nonbooli  30904  chpssati  31616  nn0difffzod  32016  hashxpe  32019  hasheuni  33083  ddemeas  33234  bnj1143  33801  distel  34775  linedegen  35115  ordcmp  35332  bj-babygodel  35481  bj-nexrt  35570  bj-csbprc  35790  onsucuni3  36248  finxpnom  36282  wl-ifp-ncond1  36345  wl-ax11-lem8  36454  unccur  36471  matunitlindflem1  36484  poimirlem26  36514  poimirlem27  36515  poimirlem31  36519  cnambfre  36536  ibladdnclem  36544  frinfm  36603  tsbi3  37003  mopickr  37232  ax13fromc9  37776  axc711  37784  axc711toc7  37786  axc5c711toc7  37790  equidqe  37792  equidq  37794  ax12indalem  37815  hdmap1eulem  40693  hdmapevec  40706  jm2.22  41734  clsk1indlem2  42793  nanorxor  43064  binomcxplemfrat  43110  binomcxplemradcnv  43111  pm10.251  43119  axc5c4c711toc7  43163  en3lpVD  43606  ax6e2ndeqVD  43670  2sb5ndVD  43671  ax6e2ndeqALT  43692  2sb5ndALT  43693  sineq0ALT  43698  nel1nelin  43835  nel2nelin  43836  axccdom  43921  fzdifsuc2  44020  liminf0  44509  cncfiooicc  44610  itgcoscmulx  44685  sge0sn  45095  isomenndlem  45246  hoidmvlelem2  45312  et-ltneverrefl  45587  singoutnword  45596  nabctnabc  45641  dfafv2  45840  afv2ndefb  45932  spr0el  46150  prmdvdsfmtnof1lem2  46253