Theorem pm2.61ne 3015

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

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

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 2931

This theorem is referenced by:  pwdom  9055  cantnfle  9578  cantnflem1  9596  cantnf  9600  djulepw  10101  infmap2  10125  zornn0g  10413  ttukeylem6  10422  msqge0  11656  xrsupsslem  13220  xrinfmsslem  13221  fzoss1  13600  swrdcl  14567  pfxcl  14599  abs1m  15257  fsumcvg3  15650  bezoutlem4  16467  dvdssq  16492  lcmid  16534  pcdvdsb  16795  pcgcd1  16803  pc2dvds  16805  pcaddlem  16814  qexpz  16827  4sqlem19  16889  prmlem1a  17032  gsumwsubmcl  18760  gsumccat  18764  gsumwmhm  18768  cntzsdrg  20733  zringlpir  21420  psdmul  22107  mretopd  23034  ufildom1  23868  alexsublem  23986  nmolb2d  24660  nmoi  24670  nmoix  24671  ipcau2  25188  mdegcl  26028  ply1divex  26096  ig1pcl  26138  dgrmulc  26231  mulcxplem  26647  vmacl  27082  efvmacl  27084  vmalelog  27170  padicabv  27595  nmlnoubi  30820  nmblolbii  30823  blocnilem  30828  blocni  30829  ubthlem1  30894  nmbdoplbi  32048  cnlnadjlem7  32097  branmfn  32129  pjbdlni  32173  shatomistici  32385  segcon2  36248  lssats  39211  ps-1  39676  3atlem5  39686  lplnnle2at  39740  2llnm3N  39768  lvolnle3at  39781  4atex2  40276  cdlemd5  40401  cdleme21k  40537  cdlemg33b  40906  mapdrvallem2  41844  mapdhcl  41926  hdmapval3N  42037  hdmap10  42039  hdmaprnlem17N  42062  hdmap14lem2a  42066  hdmaplkr  42112  hgmapvv  42125  explt1d  42520  fiabv  42733