Theorem pm2.61ne 3011

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 3009	1 ⊢ (𝜑 → 𝜓)

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

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 2927

This theorem is referenced by:  pwdom  9099  cantnfle  9631  cantnflem1  9649  cantnf  9653  djulepw  10153  infmap2  10177  zornn0g  10465  ttukeylem6  10474  msqge0  11706  xrsupsslem  13274  xrinfmsslem  13275  fzoss1  13654  swrdcl  14617  pfxcl  14649  abs1m  15309  fsumcvg3  15702  bezoutlem4  16519  dvdssq  16544  lcmid  16586  pcdvdsb  16847  pcgcd1  16855  pc2dvds  16857  pcaddlem  16866  qexpz  16879  4sqlem19  16941  prmlem1a  17084  gsumwsubmcl  18771  gsumccat  18775  gsumwmhm  18779  cntzsdrg  20718  zringlpir  21384  psdmul  22060  mretopd  22986  ufildom1  23820  alexsublem  23938  nmolb2d  24613  nmoi  24623  nmoix  24624  ipcau2  25141  mdegcl  25981  ply1divex  26049  ig1pcl  26091  dgrmulc  26184  mulcxplem  26600  vmacl  27035  efvmacl  27037  vmalelog  27123  padicabv  27548  nmlnoubi  30732  nmblolbii  30735  blocnilem  30740  blocni  30741  ubthlem1  30806  nmbdoplbi  31960  cnlnadjlem7  32009  branmfn  32041  pjbdlni  32085  shatomistici  32297  segcon2  36100  lssats  39012  ps-1  39478  3atlem5  39488  lplnnle2at  39542  2llnm3N  39570  lvolnle3at  39583  4atex2  40078  cdlemd5  40203  cdleme21k  40339  cdlemg33b  40708  mapdrvallem2  41646  mapdhcl  41728  hdmapval3N  41839  hdmap10  41841  hdmaprnlem17N  41864  hdmap14lem2a  41868  hdmaplkr  41914  hgmapvv  41927  explt1d  42318  fiabv  42531