Theorem pm2.61ne 3044

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

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

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 2960

This theorem is used by:  pwdom  9186  cantnfle  9709  cantnflem1  9727  cantnf  9731  djulepw  10310  infmap2  10334  zornn0g  10622  ttukeylem6  10631  msqge0  11877  xrsupsslem  13477  xrinfmsslem  13478  fzoss1  13861  swrdcl  14835  pfxcl  14869  abs1m  15546  fsumcvg3  15939  bezoutlem4  16759  dvdssq  16786  lcmid  16828  pcdvdsb  17091  pcgcd1  17099  pc2dvds  17101  pcaddlem  17110  qexpz  17123  4sqlem19  17185  prmlem1a  17328  gsumwsubmcl  19083  gsumccat  19087  gsumwmhm  19091  cntzsdrg  21110  zringlpir  21828  psdmul  22542  mretopd  23465  ufildom1  24300  alexsublem  24418  nmolb2d  25092  nmoi  25102  nmoix  25103  ipcau2  25610  mdegcl  26442  ply1divex  26510  ig1pcl  26552  dgrmulc  26645  mulcxplem  27069  vmacl  27502  efvmacl  27504  vmalelog  27589  padicabv  28014  nmlnoubi  31455  nmblolbii  31458  blocnilem  31463  blocni  31464  ubthlem1  31529  nmbdoplbi  32683  cnlnadjlem7  32732  branmfn  32764  pjbdlni  32808  shatomistici  33020  segcon2  37085  mh-inf3f1  37544  lssats  40335  ps-1  40800  3atlem5  40810  lplnnle2at  40864  2llnm3N  40892  lvolnle3at  40905  4atex2  41400  cdlemd5  41525  cdleme21k  41661  cdlemg33b  42030  mapdrvallem2  42968  mapdhcl  43050  hdmapval3N  43161  hdmap10  43163  hdmaprnlem17N  43186  hdmap14lem2a  43190  hdmaplkr  43236  hgmapvv  43249  explt1d  43646  fiabv  43866