Theorem pm2.61ne 3017

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

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

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 2933

This theorem is referenced by:  pwdom  9057  cantnfle  9580  cantnflem1  9598  cantnf  9602  djulepw  10103  infmap2  10127  zornn0g  10415  ttukeylem6  10424  msqge0  11658  xrsupsslem  13222  xrinfmsslem  13223  fzoss1  13602  swrdcl  14569  pfxcl  14601  abs1m  15259  fsumcvg3  15652  bezoutlem4  16469  dvdssq  16494  lcmid  16536  pcdvdsb  16797  pcgcd1  16805  pc2dvds  16807  pcaddlem  16816  qexpz  16829  4sqlem19  16891  prmlem1a  17034  gsumwsubmcl  18762  gsumccat  18766  gsumwmhm  18770  cntzsdrg  20735  zringlpir  21422  psdmul  22109  mretopd  23036  ufildom1  23870  alexsublem  23988  nmolb2d  24662  nmoi  24672  nmoix  24673  ipcau2  25190  mdegcl  26030  ply1divex  26098  ig1pcl  26140  dgrmulc  26233  mulcxplem  26649  vmacl  27084  efvmacl  27086  vmalelog  27172  padicabv  27597  nmlnoubi  30871  nmblolbii  30874  blocnilem  30879  blocni  30880  ubthlem1  30945  nmbdoplbi  32099  cnlnadjlem7  32148  branmfn  32180  pjbdlni  32224  shatomistici  32436  segcon2  36299  lssats  39272  ps-1  39737  3atlem5  39747  lplnnle2at  39801  2llnm3N  39829  lvolnle3at  39842  4atex2  40337  cdlemd5  40462  cdleme21k  40598  cdlemg33b  40967  mapdrvallem2  41905  mapdhcl  41987  hdmapval3N  42098  hdmap10  42100  hdmaprnlem17N  42123  hdmap14lem2a  42127  hdmaplkr  42173  hgmapvv  42186  explt1d  42578  fiabv  42791