Theorem pm2.61ne 3030

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ≠ wne 2943

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 206  df-an 397  df-ne 2944

This theorem is referenced by:  pwdom  8904  cantnfle  9417  cantnflem1  9435  cantnf  9439  djulepw  9936  infmap2  9962  zornn0g  10249  ttukeylem6  10258  msqge0  11484  xrsupsslem  13029  xrinfmsslem  13030  fzoss1  13402  swrdcl  14346  pfxcl  14378  abs1m  15035  fsumcvg3  15429  bezoutlem4  16238  gcdmultiplezOLD  16249  dvdssq  16260  lcmid  16302  pcdvdsb  16558  pcgcd1  16566  pc2dvds  16568  pcaddlem  16577  qexpz  16590  4sqlem19  16652  prmlem1a  16796  gsumwsubmcl  18463  gsumccatOLD  18467  gsumccat  18468  gsumwmhm  18472  cntzsdrg  20058  zringlpir  20677  mretopd  22231  ufildom1  23065  alexsublem  23183  nmolb2d  23870  nmoi  23880  nmoix  23881  ipcau2  24386  mdegcl  25222  ply1divex  25289  ig1pcl  25328  dgrmulc  25420  mulcxplem  25827  vmacl  26255  efvmacl  26257  vmalelog  26341  padicabv  26766  nmlnoubi  29144  nmblolbii  29147  blocnilem  29152  blocni  29153  ubthlem1  29218  nmbdoplbi  30372  cnlnadjlem7  30421  branmfn  30453  pjbdlni  30497  shatomistici  30709  segcon2  34393  lssats  37012  ps-1  37477  3atlem5  37487  lplnnle2at  37541  2llnm3N  37569  lvolnle3at  37582  4atex2  38077  cdlemd5  38202  cdleme21k  38338  cdlemg33b  38707  mapdrvallem2  39645  mapdhcl  39727  hdmapval3N  39838  hdmap10  39840  hdmaprnlem17N  39863  hdmap14lem2a  39867  hdmaplkr  39913  hgmapvv  39926