Theorem pm2.61ne 3040

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-ne 2956

This theorem is used by:  pwdom  9128  cantnfle  9651  cantnflem1  9669  cantnf  9673  djulepw  10196  infmap2  10220  zornn0g  10508  ttukeylem6  10517  msqge0  11760  xrsupsslem  13360  xrinfmsslem  13361  fzoss1  13743  swrdcl  14714  pfxcl  14748  abs1m  15424  fsumcvg3  15816  bezoutlem4  16633  dvdssq  16658  lcmid  16700  pcdvdsb  16962  pcgcd1  16970  pc2dvds  16972  pcaddlem  16981  qexpz  16994  4sqlem19  17056  prmlem1a  17199  gsumwsubmcl  18947  gsumccat  18951  gsumwmhm  18955  cntzsdrg  20969  zringlpir  21681  psdmul  22395  mretopd  23318  ufildom1  24153  alexsublem  24271  nmolb2d  24945  nmoi  24955  nmoix  24956  ipcau2  25463  mdegcl  26295  ply1divex  26363  ig1pcl  26405  dgrmulc  26498  mulcxplem  26922  vmacl  27355  efvmacl  27357  vmalelog  27442  padicabv  27867  nmlnoubi  31278  nmblolbii  31281  blocnilem  31286  blocni  31287  ubthlem1  31352  nmbdoplbi  32506  cnlnadjlem7  32555  branmfn  32587  pjbdlni  32631  shatomistici  32843  segcon2  36686  lssats  39886  ps-1  40351  3atlem5  40361  lplnnle2at  40415  2llnm3N  40443  lvolnle3at  40456  4atex2  40951  cdlemd5  41076  cdleme21k  41212  cdlemg33b  41581  mapdrvallem2  42519  mapdhcl  42601  hdmapval3N  42712  hdmap10  42714  hdmaprnlem17N  42737  hdmap14lem2a  42741  hdmaplkr  42787  hgmapvv  42800  explt1d  43199  fiabv  43419