Theorem pm2.61ne 3056

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 385   = wceq 1653   ≠ wne 2971

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 199  df-an 386  df-ne 2972

This theorem is referenced by:  pwdom  8354  cantnfle  8818  cantnflem1  8836  cantnf  8840  cdalepw  9306  infmap2  9328  zornn0g  9615  ttukeylem6  9624  msqge0  10841  xrsupsslem  12386  xrinfmsslem  12387  fzoss1  12750  swrdcl  13669  pfxcl  13720  abs1m  14416  fsumcvg3  14801  bezoutlem4  15594  gcdmultiplez  15605  dvdssq  15615  lcmid  15657  pcdvdsb  15906  pcgcd1  15914  pc2dvds  15916  pcaddlem  15925  qexpz  15938  4sqlem19  16000  prmlem1a  16141  gsumwsubmcl  17690  gsumccat  17693  gsumwmhm  17698  zringlpir  20159  mretopd  21225  ufildom1  22058  alexsublem  22176  nmolb2d  22850  nmoi  22860  nmoix  22861  ipcau2  23360  mdegcl  24170  ply1divex  24237  ig1pcl  24276  dgrmulc  24368  mulcxplem  24771  vmacl  25196  efvmacl  25198  vmalelog  25282  padicabv  25671  nmlnoubi  28176  nmblolbii  28179  blocnilem  28184  blocni  28185  ubthlem1  28251  nmbdoplbi  29408  cnlnadjlem7  29457  branmfn  29489  pjbdlni  29533  shatomistici  29745  segcon2  32725  lssats  35033  ps-1  35498  3atlem5  35508  lplnnle2at  35562  2llnm3N  35590  lvolnle3at  35603  4atex2  36098  cdlemd5  36223  cdleme21k  36359  cdlemg33b  36728  mapdrvallem2  37666  mapdhcl  37748  hdmapval3N  37859  hdmap10  37861  hdmaprnlem17N  37884  hdmap14lem2a  37888  hdmaplkr  37934  hgmapvv  37947  cntzsdrg  38557