Theorem pm2.61ne 3010

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

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

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 2926

This theorem is referenced by:  pwdom  9070  cantnfle  9600  cantnflem1  9618  cantnf  9622  djulepw  10122  infmap2  10146  zornn0g  10434  ttukeylem6  10443  msqge0  11675  xrsupsslem  13243  xrinfmsslem  13244  fzoss1  13623  swrdcl  14586  pfxcl  14618  abs1m  15278  fsumcvg3  15671  bezoutlem4  16488  dvdssq  16513  lcmid  16555  pcdvdsb  16816  pcgcd1  16824  pc2dvds  16826  pcaddlem  16835  qexpz  16848  4sqlem19  16910  prmlem1a  17053  gsumwsubmcl  18746  gsumccat  18750  gsumwmhm  18754  cntzsdrg  20722  zringlpir  21409  psdmul  22086  mretopd  23012  ufildom1  23846  alexsublem  23964  nmolb2d  24639  nmoi  24649  nmoix  24650  ipcau2  25167  mdegcl  26007  ply1divex  26075  ig1pcl  26117  dgrmulc  26210  mulcxplem  26626  vmacl  27061  efvmacl  27063  vmalelog  27149  padicabv  27574  nmlnoubi  30775  nmblolbii  30778  blocnilem  30783  blocni  30784  ubthlem1  30849  nmbdoplbi  32003  cnlnadjlem7  32052  branmfn  32084  pjbdlni  32128  shatomistici  32340  segcon2  36086  lssats  38998  ps-1  39464  3atlem5  39474  lplnnle2at  39528  2llnm3N  39556  lvolnle3at  39569  4atex2  40064  cdlemd5  40189  cdleme21k  40325  cdlemg33b  40694  mapdrvallem2  41632  mapdhcl  41714  hdmapval3N  41825  hdmap10  41827  hdmaprnlem17N  41850  hdmap14lem2a  41854  hdmaplkr  41900  hgmapvv  41913  explt1d  42304  fiabv  42517