Theorem con3i 157

Description: A contraposition inference. Inference associated with con3 156. 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 22	. 2 ⊢ (¬ 𝜓 → ¬ 𝜓)
2		con3i.a	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	nsyl 142	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  173  pm2.65i  197  pm5.21ni  382  pm2.45  879  pm2.46  880  con3ALT  1082  rb-ax2  1755  rb-ax4  1757  emptyex  1908  naev  2065  ax13ALT  2436  sbequiALT  2572  barocoALT  2739  necon3bi  3013  prcnel  3465  sbc2or  3729  difrab  4229  sbcel12  4316  sbcne12  4320  sbcel2  4323  ifeqor  4474  ifan  4476  nelpri  4554  nelprd  4556  eqoreldif  4582  snexALT  5249  csbopab  5407  nprrel12  5574  csbxp  5614  soirri  5953  predpoirr  6144  predfrirr  6145  nsuceq0  6239  csbiota  6317  eldifpw  7470  nlimsucg  7537  tfindsg  7555  findsg  7590  curry1val  7783  curry2val  7787  fiprc  8578  sdomirr  8638  domtriord  8647  2pwuninel  8656  mapdom1  8666  nfielex  8731  relprcnfsupp  8820  wemapso2  9001  card2inf  9003  en2lp  9053  wemapwe  9144  rankxplim3  9294  fidomtri2  9407  alephnbtwn  9482  kmlem2  9562  isfin7-2  9807  dominf  9856  ac6n  9896  alephval2  9983  dominfac  9984  gchdomtri  10040  nlt1pi  10317  zeo  12056  bcpasc  13677  hashnemnf  13700  hasheq0  13720  hashunx  13743  hashbc  13807  pfxval0  14029  flodddiv4lt  15756  prmreclem4  16245  ressinbas  16552  natfval  17208  fucbas  17222  fuchom  17223  coafval  17316  efgval  18835  gsum2dlem1  19083  gsum2dlem2  19084  dprddomprc  19115  dprdval0prc  19117  psrvscafval  20628  mavmul0g  21158  mdetralt  21213  mdetunilem9  21225  cfinfil  22498  pcofval  23615  i1fima2  24283  i1fd  24285  itgeq2  24381  ibladdlem  24423  nbgrnself2  27150  clwwlknondisj  27896  nfrgr2v  28057  avril1  28248  nmobndseqi  28562  nonbooli  29434  chpssati  30146  hashxpe  30555  hasheuni  31454  ddemeas  31605  bnj1143  32172  distel  33161  linedegen  33717  ordcmp  33908  bj-babygodel  34050  bj-nexrt  34139  bj-csbprc  34350  onsucuni3  34784  finxpnom  34818  wl-ifp-ncond1  34881  wl-ax11-lem8  34989  unccur  35040  matunitlindflem1  35053  poimirlem26  35083  poimirlem27  35084  poimirlem31  35088  cnambfre  35105  ibladdnclem  35113  frinfm  35173  tsbi3  35573  ax13fromc9  36202  axc711  36210  axc711toc7  36212  axc5c711toc7  36216  equidqe  36218  equidq  36220  ax12indalem  36241  hdmap1eulem  39118  hdmapevec  39131  jm2.22  39936  clsk1indlem2  40745  nanorxor  41009  binomcxplemfrat  41055  binomcxplemradcnv  41056  pm10.251  41064  axc5c4c711toc7  41108  en3lpVD  41551  ax6e2ndeqVD  41615  2sb5ndVD  41616  ax6e2ndeqALT  41637  2sb5ndALT  41638  sineq0ALT  41643  nel1nelin  41783  nel2nelin  41784  axccdom  41853  fzdifsuc2  41942  liminf0  42435  cncfiooicc  42536  itgcoscmulx  42611  sge0sn  43018  isomenndlem  43169  hoidmvlelem2  43235  nabctnabc  43524  dfafv2  43688  afv2ndefb  43780  spr0el  43999  prmdvdsfmtnof1lem2  44102