Theorem pm2.61ne 3045

Description: Deduction eliminating an inequality in an antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)

Hypotheses

Ref	Expression
pm2.61ne.1	⊢ (𝐴 = 𝐵 → (𝜓 ↔ 𝜒))
pm2.61ne.2	⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓)
pm2.61ne.3	⊢ (𝜑 → 𝜒)

Assertion

Ref	Expression
pm2.61ne	⊢ (𝜑 → 𝜓)

Proof of Theorem pm2.61ne

Step	Hyp	Ref	Expression
1		pm2.61ne.3	. . 3 ⊢ (𝜑 → 𝜒)
2		pm2.61ne.1	. . 3 ⊢ (𝐴 = 𝐵 → (𝜓 ↔ 𝜒))
3	1, 2	imbitrrid 249	. 2 ⊢ (𝐴 = 𝐵 → (𝜑 → 𝜓))
4		pm2.61ne.2	. . 3 ⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓)
5	4	expcom 419	. 2 ⊢ (𝐴 ≠ 𝐵 → (𝜑 → 𝜓))
6	3, 5	pm2.61ine 3043	1 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ≠ wne 2960

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-ne 2961

This theorem is used by:  pwdom  9124  cantnfle  9647  cantnflem1  9665  cantnf  9669  djulepw  10192  infmap2  10216  zornn0g  10504  ttukeylem6  10513  msqge0  11752  xrsupsslem  13351  xrinfmsslem  13352  fzoss1  13734  swrdcl  14705  pfxcl  14739  abs1m  15413  fsumcvg3  15805  bezoutlem4  16624  dvdssq  16649  lcmid  16691  pcdvdsb  16953  pcgcd1  16961  pc2dvds  16963  pcaddlem  16972  qexpz  16985  4sqlem19  17047  prmlem1a  17190  gsumwsubmcl  18935  gsumccat  18939  gsumwmhm  18943  cntzsdrg  20957  zringlpir  21669  psdmul  22381  mretopd  23301  ufildom1  24136  alexsublem  24254  nmolb2d  24928  nmoi  24938  nmoix  24939  ipcau2  25446  mdegcl  26279  ply1divex  26347  ig1pcl  26389  dgrmulc  26481  mulcxplem  26902  vmacl  27335  efvmacl  27337  vmalelog  27422  padicabv  27847  nmlnoubi  31221  nmblolbii  31224  blocnilem  31229  blocni  31230  ubthlem1  31295  nmbdoplbi  32449  cnlnadjlem7  32498  branmfn  32530  pjbdlni  32574  shatomistici  32786  segcon2  36636  lssats  39846  ps-1  40311  3atlem5  40321  lplnnle2at  40375  2llnm3N  40403  lvolnle3at  40416  4atex2  40911  cdlemd5  41036  cdleme21k  41172  cdlemg33b  41541  mapdrvallem2  42479  mapdhcl  42561  hdmapval3N  42672  hdmap10  42674  hdmaprnlem17N  42697  hdmap14lem2a  42701  hdmaplkr  42747  hgmapvv  42760  explt1d  43144  fiabv  43364