Theorem pm2.61ne 3031

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ≠ wne 2944

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 206  df-an 397  df-ne 2945

This theorem is referenced by:  pwdom  8925  cantnfle  9438  cantnflem1  9456  cantnf  9460  djulepw  9957  infmap2  9983  zornn0g  10270  ttukeylem6  10279  msqge0  11505  xrsupsslem  13050  xrinfmsslem  13051  fzoss1  13423  swrdcl  14367  pfxcl  14399  abs1m  15056  fsumcvg3  15450  bezoutlem4  16259  gcdmultiplezOLD  16270  dvdssq  16281  lcmid  16323  pcdvdsb  16579  pcgcd1  16587  pc2dvds  16589  pcaddlem  16598  qexpz  16611  4sqlem19  16673  prmlem1a  16817  gsumwsubmcl  18484  gsumccatOLD  18488  gsumccat  18489  gsumwmhm  18493  cntzsdrg  20079  zringlpir  20698  mretopd  22252  ufildom1  23086  alexsublem  23204  nmolb2d  23891  nmoi  23901  nmoix  23902  ipcau2  24407  mdegcl  25243  ply1divex  25310  ig1pcl  25349  dgrmulc  25441  mulcxplem  25848  vmacl  26276  efvmacl  26278  vmalelog  26362  padicabv  26787  nmlnoubi  29167  nmblolbii  29170  blocnilem  29175  blocni  29176  ubthlem1  29241  nmbdoplbi  30395  cnlnadjlem7  30444  branmfn  30476  pjbdlni  30520  shatomistici  30732  segcon2  34416  lssats  37033  ps-1  37498  3atlem5  37508  lplnnle2at  37562  2llnm3N  37590  lvolnle3at  37603  4atex2  38098  cdlemd5  38223  cdleme21k  38359  cdlemg33b  38728  mapdrvallem2  39666  mapdhcl  39748  hdmapval3N  39859  hdmap10  39861  hdmaprnlem17N  39884  hdmap14lem2a  39888  hdmaplkr  39934  hgmapvv  39947