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  1754  rb-ax4  1756  emptyex  1908  excomimw  2045  naev  2063  ax13ALT  2425  barocoALT  2672  necon3bi  2954  prcnel  3462  sbc2or  3745  nel1nelin  4152  nel2nelin  4153  difrab  4263  sbcel12  4356  sbcne12  4360  sbcel2  4363  rexn0  4456  ifeqor  4522  ifan  4524  nelpri  4603  nelprd  4605  eqoreldif  4633  snexALT  5316  csbopab  5490  nprrel12  5669  csbxp  5711  soirri  6068  predpoirr  6275  predfrirr  6276  nsuceq0  6386  csbiota  6469  eldifpw  7696  nlimsucg  7767  tfindsg  7786  findsg  7822  curry1val  8030  curry2val  8034  fsetdmprc0  8774  fiprc  8961  sdomirr  9022  domtriord  9031  2pwuninel  9040  mapdom1  9050  nfielex  9153  relprcnfsupp  9243  wemapso2  9434  card2inf  9436  en2lp  9491  wemapwe  9582  rankxplim3  9769  fidomtri2  9882  alephnbtwn  9957  kmlem2  10038  isfin7-2  10282  dominf  10331  ac6n  10371  alephval2  10458  dominfac  10459  gchdomtri  10515  nlt1pi  10792  zeo  12554  bcpasc  14223  hashnemnf  14246  hasheq0  14265  hashunx  14288  hashbc  14355  pfxval0  14579  flodddiv4lt  16323  prmreclem4  16826  ressinbas  17151  natfval  17851  fucbas  17865  fuchom  17866  coafval  17966  efgval  19624  gsum2dlem1  19877  gsum2dlem2  19878  dprddomprc  19909  dprdval0prc  19911  psrvscafval  21880  mavmul0g  22463  mdetralt  22518  mdetunilem9  22530  cfinfil  23803  pcofval  24932  i1fima2  25602  i1fd  25604  itgeq2  25701  ibladdlem  25743  nbgrnself2  29333  clwwlknondisj  30083  nfrgr2v  30244  avril1  30435  nmobndseqi  30751  nonbooli  31623  chpssati  32335  nn0difffzod  32778  hashxpe  32781  gsumfs2d  33027  1arithufdlem4  33504  hasheuni  34090  ddemeas  34241  bnj1143  34794  fineqvnttrclse  35136  distel  35837  linedegen  36177  ordcmp  36481  bj-babygodel  36637  bj-nexrt  36726  bj-csbprc  36944  onsucuni3  37401  finxpnom  37435  wl-ifp-ncond1  37498  wl-ax11-lem8  37626  unccur  37643  matunitlindflem1  37656  poimirlem26  37686  poimirlem27  37687  poimirlem31  37691  cnambfre  37708  ibladdnclem  37716  frinfm  37775  tsbi3  38175  mopickr  38391  ax13fromc9  38945  axc711  38953  axc711toc7  38955  axc5c711toc7  38959  equidqe  38961  equidq  38963  ax12indalem  38984  hdmap1eulem  41861  hdmapevec  41874  intnanrt  42239  jm2.22  43028  clsk1indlem2  44075  nanorxor  44338  binomcxplemfrat  44384  binomcxplemradcnv  44385  pm10.251  44393  axc5c4c711toc7  44437  en3lpVD  44877  ax6e2ndeqVD  44941  2sb5ndVD  44942  ax6e2ndeqALT  44963  2sb5ndALT  44964  sineq0ALT  44969  axccdom  45259  fzdifsuc2  45351  liminf0  45831  cncfiooicc  45932  itgcoscmulx  46007  sge0sn  46417  isomenndlem  46568  hoidmvlelem2  46634  et-ltneverrefl  46909  nabctnabc  46962  dfafv2  47163  afv2ndefb  47255  spr0el  47513  prmdvdsfmtnof1lem2  47616  fucofvalne  49357