Theorem pm2.61ne 3010

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 246	. 2 ⊢ (𝐴 = 𝐵 → (𝜑 → 𝜓))
4		pm2.61ne.2	. . 3 ⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓)
5	4	expcom 413	. 2 ⊢ (𝐴 ≠ 𝐵 → (𝜑 → 𝜓))
6	3, 5	pm2.61ine 3008	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ≠ wne 2925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-ne 2926

This theorem is referenced by:  pwdom  9093  cantnfle  9624  cantnflem1  9642  cantnf  9646  djulepw  10146  infmap2  10170  zornn0g  10458  ttukeylem6  10467  msqge0  11699  xrsupsslem  13267  xrinfmsslem  13268  fzoss1  13647  swrdcl  14610  pfxcl  14642  abs1m  15302  fsumcvg3  15695  bezoutlem4  16512  dvdssq  16537  lcmid  16579  pcdvdsb  16840  pcgcd1  16848  pc2dvds  16850  pcaddlem  16859  qexpz  16872  4sqlem19  16934  prmlem1a  17077  gsumwsubmcl  18764  gsumccat  18768  gsumwmhm  18772  cntzsdrg  20711  zringlpir  21377  psdmul  22053  mretopd  22979  ufildom1  23813  alexsublem  23931  nmolb2d  24606  nmoi  24616  nmoix  24617  ipcau2  25134  mdegcl  25974  ply1divex  26042  ig1pcl  26084  dgrmulc  26177  mulcxplem  26593  vmacl  27028  efvmacl  27030  vmalelog  27116  padicabv  27541  nmlnoubi  30725  nmblolbii  30728  blocnilem  30733  blocni  30734  ubthlem1  30799  nmbdoplbi  31953  cnlnadjlem7  32002  branmfn  32034  pjbdlni  32078  shatomistici  32290  segcon2  36093  lssats  39005  ps-1  39471  3atlem5  39481  lplnnle2at  39535  2llnm3N  39563  lvolnle3at  39576  4atex2  40071  cdlemd5  40196  cdleme21k  40332  cdlemg33b  40701  mapdrvallem2  41639  mapdhcl  41721  hdmapval3N  41832  hdmap10  41834  hdmaprnlem17N  41857  hdmap14lem2a  41861  hdmaplkr  41907  hgmapvv  41920  explt1d  42311  fiabv  42524