Theorem pm2.61ne 3017

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

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

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 2933

This theorem is referenced by:  pwdom  9067  cantnfle  9592  cantnflem1  9610  cantnf  9614  djulepw  10115  infmap2  10139  zornn0g  10427  ttukeylem6  10436  msqge0  11671  xrsupsslem  13259  xrinfmsslem  13260  fzoss1  13641  swrdcl  14608  pfxcl  14640  abs1m  15298  fsumcvg3  15691  bezoutlem4  16511  dvdssq  16536  lcmid  16578  pcdvdsb  16840  pcgcd1  16848  pc2dvds  16850  pcaddlem  16859  qexpz  16872  4sqlem19  16934  prmlem1a  17077  gsumwsubmcl  18805  gsumccat  18809  gsumwmhm  18813  cntzsdrg  20779  zringlpir  21447  psdmul  22132  mretopd  23057  ufildom1  23891  alexsublem  24009  nmolb2d  24683  nmoi  24693  nmoix  24694  ipcau2  25201  mdegcl  26034  ply1divex  26102  ig1pcl  26144  dgrmulc  26236  mulcxplem  26648  vmacl  27081  efvmacl  27083  vmalelog  27168  padicabv  27593  nmlnoubi  30867  nmblolbii  30870  blocnilem  30875  blocni  30876  ubthlem1  30941  nmbdoplbi  32095  cnlnadjlem7  32144  branmfn  32176  pjbdlni  32220  shatomistici  32432  segcon2  36287  lssats  39458  ps-1  39923  3atlem5  39933  lplnnle2at  39987  2llnm3N  40015  lvolnle3at  40028  4atex2  40523  cdlemd5  40648  cdleme21k  40784  cdlemg33b  41153  mapdrvallem2  42091  mapdhcl  42173  hdmapval3N  42284  hdmap10  42286  hdmaprnlem17N  42309  hdmap14lem2a  42313  hdmaplkr  42359  hgmapvv  42372  explt1d  42755  fiabv  42981