Theorem pm2.61ne 3033

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

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

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 2947

This theorem is referenced by:  pwdom  9195  cantnfle  9740  cantnflem1  9758  cantnf  9762  djulepw  10262  infmap2  10286  zornn0g  10574  ttukeylem6  10583  msqge0  11811  xrsupsslem  13369  xrinfmsslem  13370  fzoss1  13743  swrdcl  14693  pfxcl  14725  abs1m  15384  fsumcvg3  15777  bezoutlem4  16589  dvdssq  16614  lcmid  16656  pcdvdsb  16916  pcgcd1  16924  pc2dvds  16926  pcaddlem  16935  qexpz  16948  4sqlem19  17010  prmlem1a  17154  gsumwsubmcl  18872  gsumccat  18876  gsumwmhm  18880  cntzsdrg  20825  zringlpir  21501  psdmul  22193  mretopd  23121  ufildom1  23955  alexsublem  24073  nmolb2d  24760  nmoi  24770  nmoix  24771  ipcau2  25287  mdegcl  26128  ply1divex  26196  ig1pcl  26238  dgrmulc  26331  mulcxplem  26744  vmacl  27179  efvmacl  27181  vmalelog  27267  padicabv  27692  nmlnoubi  30828  nmblolbii  30831  blocnilem  30836  blocni  30837  ubthlem1  30902  nmbdoplbi  32056  cnlnadjlem7  32105  branmfn  32137  pjbdlni  32181  shatomistici  32393  segcon2  36069  lssats  38968  ps-1  39434  3atlem5  39444  lplnnle2at  39498  2llnm3N  39526  lvolnle3at  39539  4atex2  40034  cdlemd5  40159  cdleme21k  40295  cdlemg33b  40664  mapdrvallem2  41602  mapdhcl  41684  hdmapval3N  41795  hdmap10  41797  hdmaprnlem17N  41820  hdmap14lem2a  41824  hdmaplkr  41870  hgmapvv  41883  explt1d  42310  fiabv  42491