Theorem con3i 154

Description: A contraposition inference. Inference associated with con3 153. Its associated inference is mto 199. (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.65iOLD  196  pm5.21ni  379  pm2.45  892  pm2.46  893  con3ALT  1095  rb-ax2  1772  rb-ax4  1774  emptyex  1926  excomimw  2063  naev  2081  ax13ALT  2455  barocoALT  2702  necon3bi  2982  prcnel  3478  sbc2or  3751  nel1nelin  4157  nel2nelin  4158  difrab  4268  sbcel12  4362  sbcne12  4366  sbcel2  4369  rexn0  4447  ifeqor  4529  ifan  4531  nelpri  4611  nelprd  4613  eqoreldif  4641  vneqv  5263  snexALT  5337  csbopab  5522  nprrel12  5701  csbxp  5744  soirri  6109  predpoirr  6315  predfrirr  6316  nsuceq0  6426  csbiota  6509  eldifpw  7746  nlimsucg  7817  tfindsg  7836  findsg  7873  curry1val  8078  curry2val  8082  fsetdmprc0  8830  fiprc  9019  sdomirr  9080  domtriord  9089  2pwuninel  9098  mapdom1  9108  nfielex  9212  relprcnfsupp  9304  wemapso2  9495  card2inf  9497  en2lp  9555  wemapwe  9646  rankxplim3  9833  fidomtri2  9946  alephnbtwn  10021  kmlem2  10102  isfin7-2  10347  dominf  10396  ac6n  10436  alephval2  10524  dominfac  10525  gchdomtri  10581  nlt1pi  10858  indval0  12193  zeo  12653  bcpasc  14328  hashnemnf  14351  hasheq0  14370  hashunx  14393  hashbc  14460  pfxval0  14684  flodddiv4lt  16442  prmreclem4  16946  ressinbas  17272  natfval  17973  fucbas  17987  fuchom  17988  coafval  18088  efgval  19748  gsum2dlem1  20001  gsum2dlem2  20002  dprddomprc  20033  dprdval0prc  20035  psrvscafval  21988  mavmul0g  22601  mdetralt  22656  mdetunilem9  22668  cfinfil  23941  pcofval  25060  i1fima2  25729  i1fd  25731  itgeq2  25828  ibladdlem  25870  nbgrnself2  29518  clwwlknondisj  30270  nfrgr2v  30431  avril1  30622  nmobndseqi  30939  nonbooli  31811  chpssati  32523  nn0difffzod  32967  hashxpe  32970  gsumfs2d  33202  1arithufdlem4  33704  hasheuni  34343  ddemeas  34494  bnj1143  35046  fineqvnttrclse  35381  fineqvinfep  35382  distel  36112  linedegen  36454  ordcmp  36768  bj-babygodel  37007  bj-nexrt  37128  bj-csbprc  37356  onsucuni3  37822  finxpnom  37856  wl-ifp-ncond1  37919  unccur  38063  matunitlindflem1  38076  poimirlem26  38106  poimirlem27  38107  poimirlem31  38111  cnambfre  38128  ibladdnclem  38136  frinfm  38195  tsbi3  38595  mopickr  38831  ax13fromc9  39491  axc711  39499  axc711toc7  39501  axc5c711toc7  39505  equidqe  39507  equidq  39509  ax12indalem  39530  hdmap1eulem  42407  hdmapevec  42420  intnanrt  42784  jm2.22  43533  clsk1indlem2  44579  nanorxor  44842  binomcxplemfrat  44888  binomcxplemradcnv  44889  pm10.251  44897  axc5c4c711toc7  44941  en3lpVD  45381  ax6e2ndeqVD  45445  2sb5ndVD  45446  ax6e2ndeqALT  45467  2sb5ndALT  45468  sineq0ALT  45473  axccdom  45759  fzdifsuc2  45850  liminf0  46328  cncfiooicc  46429  itgcoscmulx  46504  sge0sn  46914  isomenndlem  47065  hoidmvlelem2  47131  et-ltneverrefl  47406  quantgodelALT  47410  nabctnabc  47486  dfafv2  47687  afv2ndefb  47779  spr0el  48049  prmdvdsfmtnof1lem2  48155  fucofvalne  49907