Theorem pm2.61ne 3028

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ≠ wne 2941

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 398  df-ne 2942

This theorem is referenced by:  pwdom  9129  cantnfle  9666  cantnflem1  9684  cantnf  9688  djulepw  10187  infmap2  10213  zornn0g  10500  ttukeylem6  10509  msqge0  11735  xrsupsslem  13286  xrinfmsslem  13287  fzoss1  13659  swrdcl  14595  pfxcl  14627  abs1m  15282  fsumcvg3  15675  bezoutlem4  16484  dvdssq  16504  lcmid  16546  pcdvdsb  16802  pcgcd1  16810  pc2dvds  16812  pcaddlem  16821  qexpz  16834  4sqlem19  16896  prmlem1a  17040  gsumwsubmcl  18718  gsumccat  18722  gsumwmhm  18726  cntzsdrg  20418  zringlpir  21037  mretopd  22596  ufildom1  23430  alexsublem  23548  nmolb2d  24235  nmoi  24245  nmoix  24246  ipcau2  24751  mdegcl  25587  ply1divex  25654  ig1pcl  25693  dgrmulc  25785  mulcxplem  26192  vmacl  26622  efvmacl  26624  vmalelog  26708  padicabv  27133  nmlnoubi  30049  nmblolbii  30052  blocnilem  30057  blocni  30058  ubthlem1  30123  nmbdoplbi  31277  cnlnadjlem7  31326  branmfn  31358  pjbdlni  31402  shatomistici  31614  segcon2  35077  lssats  37882  ps-1  38348  3atlem5  38358  lplnnle2at  38412  2llnm3N  38440  lvolnle3at  38453  4atex2  38948  cdlemd5  39073  cdleme21k  39209  cdlemg33b  39578  mapdrvallem2  40516  mapdhcl  40598  hdmapval3N  40709  hdmap10  40711  hdmaprnlem17N  40734  hdmap14lem2a  40738  hdmaplkr  40784  hgmapvv  40797