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  1753  rb-ax4  1755  emptyex  1907  excomimw  2044  naev  2061  ax13ALT  2424  barocoALT  2671  necon3bi  2952  prcnel  3476  sbc2or  3765  nel1nelin  4173  nel2nelin  4174  difrab  4284  sbcel12  4377  sbcne12  4381  sbcel2  4384  rexn0  4477  ifeqor  4543  ifan  4545  nelpri  4622  nelprd  4624  eqoreldif  4652  snexALT  5341  csbopab  5518  nprrel12  5699  csbxp  5741  soirri  6102  predpoirr  6309  predfrirr  6310  nsuceq0  6420  csbiota  6507  eldifpw  7747  nlimsucg  7821  tfindsg  7840  findsg  7876  curry1val  8087  curry2val  8091  fsetdmprc0  8831  fiprc  9019  sdomirr  9084  domtriord  9093  2pwuninel  9102  mapdom1  9112  nfielex  9225  relprcnfsupp  9322  wemapso2  9513  card2inf  9515  en2lp  9566  wemapwe  9657  rankxplim3  9841  fidomtri2  9954  alephnbtwn  10031  kmlem2  10112  isfin7-2  10356  dominf  10405  ac6n  10445  alephval2  10532  dominfac  10533  gchdomtri  10589  nlt1pi  10866  zeo  12627  bcpasc  14293  hashnemnf  14316  hasheq0  14335  hashunx  14358  hashbc  14425  pfxval0  14648  flodddiv4lt  16394  prmreclem4  16897  ressinbas  17222  natfval  17918  fucbas  17932  fuchom  17933  coafval  18033  efgval  19654  gsum2dlem1  19907  gsum2dlem2  19908  dprddomprc  19939  dprdval0prc  19941  psrvscafval  21864  mavmul0g  22447  mdetralt  22502  mdetunilem9  22514  cfinfil  23787  pcofval  24917  i1fima2  25587  i1fd  25589  itgeq2  25686  ibladdlem  25728  nbgrnself2  29294  clwwlknondisj  30047  nfrgr2v  30208  avril1  30399  nmobndseqi  30715  nonbooli  31587  chpssati  32299  nn0difffzod  32736  hashxpe  32739  gsumfs2d  33002  1arithufdlem4  33525  hasheuni  34082  ddemeas  34233  bnj1143  34787  distel  35798  linedegen  36138  ordcmp  36442  bj-babygodel  36598  bj-nexrt  36687  bj-csbprc  36905  onsucuni3  37362  finxpnom  37396  wl-ifp-ncond1  37459  wl-ax11-lem8  37587  unccur  37604  matunitlindflem1  37617  poimirlem26  37647  poimirlem27  37648  poimirlem31  37652  cnambfre  37669  ibladdnclem  37677  frinfm  37736  tsbi3  38136  mopickr  38352  ax13fromc9  38906  axc711  38914  axc711toc7  38916  axc5c711toc7  38920  equidqe  38922  equidq  38924  ax12indalem  38945  hdmap1eulem  41823  hdmapevec  41836  intnanrt  42201  jm2.22  42991  clsk1indlem2  44038  nanorxor  44301  binomcxplemfrat  44347  binomcxplemradcnv  44348  pm10.251  44356  axc5c4c711toc7  44400  en3lpVD  44841  ax6e2ndeqVD  44905  2sb5ndVD  44906  ax6e2ndeqALT  44927  2sb5ndALT  44928  sineq0ALT  44933  axccdom  45223  fzdifsuc2  45315  liminf0  45798  cncfiooicc  45899  itgcoscmulx  45974  sge0sn  46384  isomenndlem  46535  hoidmvlelem2  46601  et-ltneverrefl  46876  singoutnword  46887  nabctnabc  46936  dfafv2  47137  afv2ndefb  47229  spr0el  47487  prmdvdsfmtnof1lem2  47590  fucofvalne  49318