Theorem pm2.61ne 3019

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547   ≠ wne 2934

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 208  df-an 397  df-ne 2935

This theorem is referenced by:  pwdom  9057  cantnfle  9583  cantnflem1  9601  cantnf  9605  djulepw  10106  infmap2  10130  zornn0g  10418  ttukeylem6  10427  msqge0  11662  xrsupsslem  13250  xrinfmsslem  13251  fzoss1  13632  swrdcl  14599  pfxcl  14631  abs1m  15289  fsumcvg3  15682  bezoutlem4  16502  dvdssq  16527  lcmid  16569  pcdvdsb  16831  pcgcd1  16839  pc2dvds  16841  pcaddlem  16850  qexpz  16863  4sqlem19  16925  prmlem1a  17068  gsumwsubmcl  18796  gsumccat  18800  gsumwmhm  18804  cntzsdrg  20774  zringlpir  21442  psdmul  22154  mretopd  23075  ufildom1  23909  alexsublem  24027  nmolb2d  24701  nmoi  24711  nmoix  24712  ipcau2  25219  mdegcl  26052  ply1divex  26120  ig1pcl  26162  dgrmulc  26254  mulcxplem  26666  vmacl  27099  efvmacl  27101  vmalelog  27186  padicabv  27611  nmlnoubi  30885  nmblolbii  30888  blocnilem  30893  blocni  30894  ubthlem1  30959  nmbdoplbi  32113  cnlnadjlem7  32162  branmfn  32194  pjbdlni  32238  shatomistici  32450  segcon2  36333  lssats  39504  ps-1  39969  3atlem5  39979  lplnnle2at  40033  2llnm3N  40061  lvolnle3at  40074  4atex2  40569  cdlemd5  40694  cdleme21k  40830  cdlemg33b  41199  mapdrvallem2  42137  mapdhcl  42219  hdmapval3N  42330  hdmap10  42332  hdmaprnlem17N  42355  hdmap14lem2a  42359  hdmaplkr  42405  hgmapvv  42418  explt1d  42800  fiabv  43022