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  378  pm2.45  878  pm2.46  879  con3ALT  1083  rb-ax2  1757  rb-ax4  1759  emptyex  1911  naev  2064  ax13ALT  2425  barocoALT  2678  necon3bi  2969  prcnel  3445  sbc2or  3720  difrab  4239  sbcel12  4339  sbcne12  4343  sbcel2  4346  rexn0  4438  ifeqor  4507  ifan  4509  nelpri  4587  nelprd  4589  eqoreldif  4617  snexALT  5301  csbopab  5461  nprrel12  5636  csbxp  5676  soirri  6020  predpoirr  6225  predfrirr  6226  nsuceq0  6331  csbiota  6411  eldifpw  7596  nlimsucg  7664  tfindsg  7682  findsg  7720  curry1val  7916  curry2val  7920  fsetdmprc0  8601  fiprc  8789  sdomirr  8850  domtriord  8859  2pwuninel  8868  mapdom1  8878  nfielex  8976  relprcnfsupp  9061  wemapso2  9242  card2inf  9244  en2lp  9294  wemapwe  9385  rankxplim3  9570  fidomtri2  9683  alephnbtwn  9758  kmlem2  9838  isfin7-2  10083  dominf  10132  ac6n  10172  alephval2  10259  dominfac  10260  gchdomtri  10316  nlt1pi  10593  zeo  12336  bcpasc  13963  hashnemnf  13986  hasheq0  14006  hashunx  14029  hashbc  14093  pfxval0  14317  flodddiv4lt  16052  prmreclem4  16548  ressinbas  16881  natfval  17578  fucbas  17593  fuchom  17594  fuchomOLD  17595  coafval  17695  efgval  19238  gsum2dlem1  19486  gsum2dlem2  19487  dprddomprc  19518  dprdval0prc  19520  psrvscafval  21069  mavmul0g  21610  mdetralt  21665  mdetunilem9  21677  cfinfil  22952  pcofval  24079  i1fima2  24748  i1fd  24750  itgeq2  24847  ibladdlem  24889  nbgrnself2  27630  clwwlknondisj  28376  nfrgr2v  28537  avril1  28728  nmobndseqi  29042  nonbooli  29914  chpssati  30626  hashxpe  31029  hasheuni  31953  ddemeas  32104  bnj1143  32670  distel  33685  linedegen  34372  ordcmp  34563  bj-babygodel  34712  bj-nexrt  34801  bj-csbprc  35022  onsucuni3  35465  finxpnom  35499  wl-ifp-ncond1  35562  wl-ax11-lem8  35670  unccur  35687  matunitlindflem1  35700  poimirlem26  35730  poimirlem27  35731  poimirlem31  35735  cnambfre  35752  ibladdnclem  35760  frinfm  35820  tsbi3  36220  ax13fromc9  36847  axc711  36855  axc711toc7  36857  axc5c711toc7  36861  equidqe  36863  equidq  36865  ax12indalem  36886  hdmap1eulem  39763  hdmapevec  39776  jm2.22  40733  clsk1indlem2  41541  nanorxor  41812  binomcxplemfrat  41858  binomcxplemradcnv  41859  pm10.251  41867  axc5c4c711toc7  41911  en3lpVD  42354  ax6e2ndeqVD  42418  2sb5ndVD  42419  ax6e2ndeqALT  42440  2sb5ndALT  42441  sineq0ALT  42446  nel1nelin  42584  nel2nelin  42585  axccdom  42651  fzdifsuc2  42739  liminf0  43224  cncfiooicc  43325  itgcoscmulx  43400  sge0sn  43807  isomenndlem  43958  hoidmvlelem2  44024  nabctnabc  44313  dfafv2  44511  afv2ndefb  44603  spr0el  44822  prmdvdsfmtnof1lem2  44925