Theorem pm2.61ne 3042

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1560   ≠ wne 2957

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 209  df-an 400  df-ne 2958

This theorem is referenced by:  pwdom  9101  cantnfle  9626  cantnflem1  9644  cantnf  9648  djulepw  10149  infmap2  10173  zornn0g  10462  ttukeylem6  10471  msqge0  11708  xrsupsslem  13310  xrinfmsslem  13311  fzoss1  13692  swrdcl  14659  pfxcl  14691  abs1m  15363  fsumcvg3  15756  bezoutlem4  16576  dvdssq  16601  lcmid  16643  pcdvdsb  16905  pcgcd1  16913  pc2dvds  16915  pcaddlem  16924  qexpz  16937  4sqlem19  16999  prmlem1a  17142  gsumwsubmcl  18871  gsumccat  18875  gsumwmhm  18879  cntzsdrg  20851  zringlpir  21519  psdmul  22231  mretopd  23152  ufildom1  23986  alexsublem  24104  nmolb2d  24778  nmoi  24788  nmoix  24789  ipcau2  25296  mdegcl  26129  ply1divex  26197  ig1pcl  26239  dgrmulc  26331  mulcxplem  26749  vmacl  27182  efvmacl  27184  vmalelog  27269  padicabv  27694  nmlnoubi  30999  nmblolbii  31002  blocnilem  31007  blocni  31008  ubthlem1  31073  nmbdoplbi  32227  cnlnadjlem7  32276  branmfn  32308  pjbdlni  32352  shatomistici  32564  segcon2  36455  lssats  39636  ps-1  40101  3atlem5  40111  lplnnle2at  40165  2llnm3N  40193  lvolnle3at  40206  4atex2  40701  cdlemd5  40826  cdleme21k  40962  cdlemg33b  41331  mapdrvallem2  42269  mapdhcl  42351  hdmapval3N  42462  hdmap10  42464  hdmaprnlem17N  42487  hdmap14lem2a  42491  hdmaplkr  42537  hgmapvv  42550  explt1d  42932  fiabv  43154