Theorem pm2.61ne 3018

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

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

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 2934

This theorem is referenced by:  pwdom  9061  cantnfle  9586  cantnflem1  9604  cantnf  9608  djulepw  10109  infmap2  10133  zornn0g  10421  ttukeylem6  10430  msqge0  11665  xrsupsslem  13253  xrinfmsslem  13254  fzoss1  13635  swrdcl  14602  pfxcl  14634  abs1m  15292  fsumcvg3  15685  bezoutlem4  16505  dvdssq  16530  lcmid  16572  pcdvdsb  16834  pcgcd1  16842  pc2dvds  16844  pcaddlem  16853  qexpz  16866  4sqlem19  16928  prmlem1a  17071  gsumwsubmcl  18799  gsumccat  18803  gsumwmhm  18807  cntzsdrg  20773  zringlpir  21460  psdmul  22145  mretopd  23070  ufildom1  23904  alexsublem  24022  nmolb2d  24696  nmoi  24706  nmoix  24707  ipcau2  25214  mdegcl  26047  ply1divex  26115  ig1pcl  26157  dgrmulc  26249  mulcxplem  26664  vmacl  27098  efvmacl  27100  vmalelog  27185  padicabv  27610  nmlnoubi  30885  nmblolbii  30888  blocnilem  30893  blocni  30894  ubthlem1  30959  nmbdoplbi  32113  cnlnadjlem7  32162  branmfn  32194  pjbdlni  32238  shatomistici  32450  segcon2  36306  lssats  39475  ps-1  39940  3atlem5  39950  lplnnle2at  40004  2llnm3N  40032  lvolnle3at  40045  4atex2  40540  cdlemd5  40665  cdleme21k  40801  cdlemg33b  41170  mapdrvallem2  42108  mapdhcl  42190  hdmapval3N  42301  hdmap10  42303  hdmaprnlem17N  42326  hdmap14lem2a  42330  hdmaplkr  42376  hgmapvv  42389  explt1d  42772  fiabv  42998