Theorem pm2.61dane 3044

Description: Deduction eliminating an inequality in an antecedent. (Contributed by NM, 30-Nov-2011.)

Hypotheses

Ref	Expression
pm2.61dane.1	⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝜓)
pm2.61dane.2	⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓)

Assertion

Ref	Expression
pm2.61dane	⊢ (𝜑 → 𝜓)

Proof of Theorem pm2.61dane

Step	Hyp	Ref	Expression
1		pm2.61dane.1	. . 3 ⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝜓)
2	1	ex 417	. 2 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓))
3		pm2.61dane.2	. . 3 ⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓)
4	3	ex 417	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓))
5	2, 4	pm2.61dne 3043	1 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   = wceq 1569   ≠ wne 2957

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401  df-ne 2958

This theorem is used by:  pm2.61da2ne  3045  pm2.61da3ne  3046  pm2.61iine  3047  disjxiun  5105  onfr  6400  f1oprswap  6866  soex  7916  frxp2  8138  frxp3  8145  riiner  8786  difsnen  9045  mapdom2  9134  nnunifi  9249  fofinf1o  9287  brwdom2  9533  cantnff  9641  cantnfp1  9648  carddomi2  9963  wdomfil  10052  fin1a2lem10  10399  fin1a2lem11  10400  uzsupss  12970  xaddcom  13272  xnegdi  13280  xpncan  13283  xleadd1a  13285  xsubge0  13293  ccat1st1st  14673  swrdccatin1  14769  sgncl  15141  cnpart  15298  fsumcllem  15790  fsumrev2  15840  expcnv  15925  geomulcvg  15937  fprodcllem  16012  fsumdvds  16372  gcd0id  16583  nn0seqcvgd  16634  lcmdvds  16672  mulgcddvds  16719  pcge0  16928  pcneg  16940  pcdvdstr  16942  pcz  16947  pcprmpw2  16948  pcadd  16955  ramcl2  17082  0ramcl  17089  ramub1lem1  17092  ramcl  17095  mrerintcl  17655  mreriincl  17656  mreexexlem4d  17709  mreclatBAD  18625  chnub  18684  psgnunilem1  19569  odmulg  19632  sylow1lem1  19674  pgpfi  19681  odadd1  19924  odadd2  19925  gsumval3  19983  gsumpt  20038  dprdfcntz  20093  dprd2da  20120  ablfac1eulem  20150  pgpfaclem3  20161  ablsimpgfind  20188  abvneg  20940  lssssr  21086  lspsneq  21257  lspdisj2  21262  drngnidl  21388  cnsubrg  21588  riinopn  23076  riincld  23212  neipeltop  23297  hauscmplem  23574  cmpfi  23576  ptbasfi  23749  xkoccn  23787  txindislem  23801  txtube  23808  hmphindis  23965  fclscmp  24198  utop2nei  24418  nrginvrcn  24860  nmoleub  24899  blcvx  24966  xrsxmet  24978  xrsblre  24980  lebnumlem3  25133  cphsqrtcl2  25356  ovollb2  25659  ioorcl  25747  i1fmulc  25873  itg1mulc  25874  mbfi1fseqlem4  25888  bddiblnc  26012  dvlip  26163  dvne0  26181  ig1pdvds  26348  plyeq0lem  26378  plyeq0  26379  aannenlem2  26503  aalioulem6  26511  abelthlem8  26613  abelth  26615  cxpexp  26844  cxpge0  26859  cxpmul2  26865  abscxp2  26869  abscxpbnd  26929  cxpeq  26933  nnlogbexp  26957  isosctrlem2  26995  atanrecl  27087  wilthlem2  27244  dchrabs2  27437  dchr1re  27438  lgsneg1  27497  lgsdirprm  27506  lgsdir  27507  lgsne0  27510  lgsdirnn0  27519  lgsdinn0  27520  2sqlem9  27602  rpvmasumlem  27662  dchrvmasumiflem1  27676  dchrisum0flblem1  27683  rpvmasum2  27687  pntrsumbnd2  27742  pntleml  27786  tgcgrextend  28765  tgbtwnexch2  28776  tgifscgr  28788  tgcolg  28834  tgidinside  28851  tgbtwnconn1lem2  28853  tgbtwnconn1lem3  28854  lnhl  28898  tglinethru  28920  tglineneq  28929  coltr  28932  coltr3  28933  colline  28934  tglnpt2  28937  tglnpt4  28939  mirreu3  28942  miriso  28958  mirln  28964  mirln2  28965  mirconn  28966  mirbtwnhl  28968  colmid  28976  krippenlem  28978  midexlem  28980  ragflat  28995  ragcgr  28998  perprag  29018  perpdragALT  29019  colperpexlem1  29022  colperpexlem3  29024  midex  29029  opphllem1  29039  opphllem2  29040  opphllem5  29043  opphllem6  29044  hlpasch  29049  lnincplng  29077  lnssplng  29085  mirplncl  29088  lmiisolem  29116  hypcgrlem1  29120  hypcgrlem2  29121  cgrg3col4  29181  prlnghpg  29207  perpprlng  29211  prlngmolem2  29214  prlngpln4  29219  prlngplngtr  29220  prlngmid2  29222  upgrex  29453  crctcshwlk  30182  crctcsh  30184  1wlkdlem2  30500  eupth2lem3lem3  30592  eupth2lem3lem7  30596  nmcoplbi  32391  nmophmi  32394  nmbdfnlbi  32412  disjdifprg  32931  imadifxp  32957  2ndimaxp  33002  mptiffisupp  33049  xlt2addrd  33115  ssnnssfz  33143  gsumpart  33392  suppgsumssiun  33401  symgcntz  33414  fzo0pmtrlast  33421  pmtridf1o  33423  pmtridfv1  33424  pmtridfv2  33425  psgnfzto1stlem  33429  tocycf  33446  cycpmco2lem5  33459  cycpmco2  33462  fxpgaval  33496  linds2eq  33703  dvdsruasso  33707  ply1coedeg  33888  ply1degltel  33893  ply1degleel  33894  ig1pmindeg  33901  esplyind  33974  fldext2chn  34127  constraddcl  34161  constrremulcl  34166  constrsqrtcl  34178  cos9thpiminplylem2  34182  locfinref  34240  zarcmplem  34280  esumpr2  34466  unelldsys  34557  sigapildsyslem  34560  sigapildsys  34561  mbfmcst  34658  carsgsigalem  34714  carsgclctunlem3  34719  pmeasmono  34723  probun  34818  0rrv  34850  signsvtn0  34966  signstfvneq0  34968  fineqvac  35537  wevgblacfn  35603  btwnconn1lem11  36597  finxp00  38076  matunitlindf  38297  poimirlem14  38313  mblfinlem1  38336  mblfinlem2  38337  ismblfin  38340  itg2addnclem  38350  itgaddnclem2  38358  areacirclem4  38390  areacirc  38392  isbnd3  38463  blbnd  38466  rrnequiv  38514  lsmsat  39810  lkrscss  39900  eqlkr  39901  lkrshpor  39909  atcvrj2b  40234  atltcvr  40237  3dim1  40269  3dim2  40270  3dim3  40271  ps-2  40280  2at0mat0  40327  dalemdnee  40468  dalem63  40537  lnatexN  40581  2llnma3r  40590  pmodlem1  40648  pmapjat1  40655  pclfinclN  40752  osumclN  40769  pexmidALTN  40780  lhpexle2lem  40811  lhpexle3lem  40813  4atexlemex6  40876  4atex  40878  trlnle  40988  trlval3  40989  cdlemc  40999  cdlemd9  41008  cdleme27N  41171  cdleme28c  41174  cdleme32fvaw  41241  cdleme42ke  41287  cdleme42keg  41288  cdleme42mgN  41290  cdleme17d  41300  cdleme48fvg  41302  cdleme50trn123  41356  cdlemb3  41408  cdlemg8  41433  cdlemg15a  41457  cdlemg15  41458  cdlemg16  41459  cdlemg16ALTN  41460  cdlemg16z  41461  cdlemg16zz  41462  cdlemg20  41487  cdlemg22  41489  cdlemg37  41491  cdlemg31d  41502  cdlemg39  41518  cdlemg40  41519  ltrncom  41540  tendotr  41632  cdlemk25-3  41706  cdlemk35s-id  41740  cdlemk39s-id  41742  cdlemk53b  41758  cdlemk53  41759  cdlemk55  41763  cdlemk35u  41766  cdlemk55u  41768  cdlemk39u  41770  cdlemk19u  41772  cdleml5N  41782  dia2dimlem7  41872  dia2dimlem13  41878  dih1dimatlem  42131  dihlsprn  42133  dihjat1lem  42230  dihjat1  42231  dvh2dim  42247  dochexmid  42270  lclkrlem1  42308  lclkrlem2i  42317  lclkrlem2t  42328  lcfrlem34  42378  lcfrlem38  42382  lcfrlem41  42385  mapdindp1  42522  mapdindp2  42523  mapdh6dN  42541  mapdh6jN  42547  mapdh8j  42589  mapdh8  42590  hdmap1l6d  42615  hdmap1l6j  42621  hdmap11lem2  42644  hdmap14lem7  42676  primrootlekpowne0  42900  aks6d1c7lem2  42976  unitscyglem4  42993  jm2.19  43748  jm2.23  43751  nzss  45055  disjxp1  45817  cnrefiisplem  46571  xlimliminflimsup  46604  stoweidlem58  46800  fourierdlem41  46890  fourierdlem48  46896  fouriersw  46973  etransclem24  47000  nnfoctbdjlem  47197  smfpimltxr  47489  smfpimgtxr  47522  chnerlem1  47626  sqrtqaa  47634  ssnn0ssfz  49157  mreclat  49803