Theorem pm2.61ne 3072

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ≠ wne 2987

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 210  df-an 400  df-ne 2988

This theorem is referenced by:  pwdom  8653  cantnfle  9118  cantnflem1  9136  cantnf  9140  djulepw  9603  infmap2  9629  zornn0g  9916  ttukeylem6  9925  msqge0  11150  xrsupsslem  12688  xrinfmsslem  12689  fzoss1  13059  swrdcl  13998  pfxcl  14030  abs1m  14687  fsumcvg3  15078  bezoutlem4  15880  gcdmultiplezOLD  15891  dvdssq  15901  lcmid  15943  pcdvdsb  16195  pcgcd1  16203  pc2dvds  16205  pcaddlem  16214  qexpz  16227  4sqlem19  16289  prmlem1a  16432  gsumwsubmcl  17993  gsumccatOLD  17997  gsumccat  17998  gsumwmhm  18002  cntzsdrg  19574  zringlpir  20182  mretopd  21697  ufildom1  22531  alexsublem  22649  nmolb2d  23324  nmoi  23334  nmoix  23335  ipcau2  23838  mdegcl  24670  ply1divex  24737  ig1pcl  24776  dgrmulc  24868  mulcxplem  25275  vmacl  25703  efvmacl  25705  vmalelog  25789  padicabv  26214  nmlnoubi  28579  nmblolbii  28582  blocnilem  28587  blocni  28588  ubthlem1  28653  nmbdoplbi  29807  cnlnadjlem7  29856  branmfn  29888  pjbdlni  29932  shatomistici  30144  segcon2  33679  lssats  36308  ps-1  36773  3atlem5  36783  lplnnle2at  36837  2llnm3N  36865  lvolnle3at  36878  4atex2  37373  cdlemd5  37498  cdleme21k  37634  cdlemg33b  38003  mapdrvallem2  38941  mapdhcl  39023  hdmapval3N  39134  hdmap10  39136  hdmaprnlem17N  39159  hdmap14lem2a  39163  hdmaplkr  39209  hgmapvv  39222