Theorem pm2.61ne 3027

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

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

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 2941

This theorem is referenced by:  pwdom  9125  cantnfle  9662  cantnflem1  9680  cantnf  9684  djulepw  10183  infmap2  10209  zornn0g  10496  ttukeylem6  10505  msqge0  11731  xrsupsslem  13282  xrinfmsslem  13283  fzoss1  13655  swrdcl  14591  pfxcl  14623  abs1m  15278  fsumcvg3  15671  bezoutlem4  16480  dvdssq  16500  lcmid  16542  pcdvdsb  16798  pcgcd1  16806  pc2dvds  16808  pcaddlem  16817  qexpz  16830  4sqlem19  16892  prmlem1a  17036  gsumwsubmcl  18714  gsumccat  18718  gsumwmhm  18722  cntzsdrg  20410  zringlpir  21028  mretopd  22587  ufildom1  23421  alexsublem  23539  nmolb2d  24226  nmoi  24236  nmoix  24237  ipcau2  24742  mdegcl  25578  ply1divex  25645  ig1pcl  25684  dgrmulc  25776  mulcxplem  26183  vmacl  26611  efvmacl  26613  vmalelog  26697  padicabv  27122  nmlnoubi  30036  nmblolbii  30039  blocnilem  30044  blocni  30045  ubthlem1  30110  nmbdoplbi  31264  cnlnadjlem7  31313  branmfn  31345  pjbdlni  31389  shatomistici  31601  segcon2  35065  lssats  37870  ps-1  38336  3atlem5  38346  lplnnle2at  38400  2llnm3N  38428  lvolnle3at  38441  4atex2  38936  cdlemd5  39061  cdleme21k  39197  cdlemg33b  39566  mapdrvallem2  40504  mapdhcl  40586  hdmapval3N  40697  hdmap10  40699  hdmaprnlem17N  40722  hdmap14lem2a  40726  hdmaplkr  40772  hgmapvv  40785