Theorem pm2.61dane 3029

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 413	. 2 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓))
3		pm2.61dane.2	. . 3 ⊢ ((𝜑 ∧ 𝐴 ≠ 𝐵) → 𝜓)
4	3	ex 413	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓))
5	2, 4	pm2.61dne 3028	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ 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:  pm2.61da2ne  3030  pm2.61da3ne  3031  pm2.61iine  3032  disjxiun  5145  onfr  6403  f1oprswap  6877  soex  7914  frxp2  8132  frxp3  8139  riiner  8786  difsnen  9055  mapdom2  9150  nnunifi  9296  fofinf1o  9329  brwdom2  9570  cantnff  9671  cantnfp1  9678  carddomi2  9967  wdomfil  10058  fin1a2lem10  10406  fin1a2lem11  10407  uzsupss  12926  xaddcom  13221  xnegdi  13229  xpncan  13232  xleadd1a  13234  xsubge0  13242  ccat1st1st  14580  swrdccatin1  14677  cnpart  15189  fsumcllem  15680  fsumrev2  15730  expcnv  15812  geomulcvg  15824  fprodcllem  15897  fsumdvds  16253  gcd0id  16462  nn0seqcvgd  16509  lcmdvds  16547  mulgcddvds  16594  pcge0  16797  pcneg  16809  pcdvdstr  16811  pcz  16816  pcprmpw2  16817  pcadd  16824  ramcl2  16951  0ramcl  16958  ramub1lem1  16961  ramcl  16964  mrerintcl  17543  mreriincl  17544  mreexexlem4d  17593  mreclatBAD  18518  psgnunilem1  19363  odmulg  19426  sylow1lem1  19468  pgpfi  19475  odadd1  19718  odadd2  19719  gsumval3  19777  gsumpt  19832  dprdfcntz  19887  dprd2da  19914  ablfac1eulem  19944  pgpfaclem3  19955  ablsimpgfind  19982  abvneg  20446  lssssr  20569  lspsneq  20741  lspdisj2  20746  drngnidl  20860  cnsubrg  21011  riinopn  22417  riincld  22555  neipeltop  22640  hauscmplem  22917  cmpfi  22919  ptbasfi  23092  xkoccn  23130  txindislem  23144  txtube  23151  hmphindis  23308  fclscmp  23541  utop2nei  23762  nrginvrcn  24216  nmoleub  24255  blcvx  24321  xrsxmet  24332  xrsblre  24334  lebnumlem3  24486  cphsqrtcl2  24710  ovollb2  25013  ioorcl  25101  i1fmulc  25228  itg1mulc  25229  mbfi1fseqlem4  25243  bddiblnc  25366  dvlip  25517  dvne0  25535  ig1pdvds  25701  plyeq0lem  25731  plyeq0  25732  aannenlem2  25849  aalioulem6  25857  abelthlem8  25958  abelth  25960  cxpexp  26183  cxpge0  26198  cxpmul2  26204  abscxp2  26208  abscxpbnd  26268  cxpeq  26272  nnlogbexp  26293  isosctrlem2  26331  atanrecl  26423  wilthlem2  26580  dchrabs2  26772  dchr1re  26773  lgsneg1  26832  lgsdirprm  26841  lgsdir  26842  lgsne0  26845  lgsdirnn0  26854  lgsdinn0  26855  2sqlem9  26937  rpvmasumlem  26997  dchrvmasumiflem1  27011  dchrisum0flblem1  27018  rpvmasum2  27022  pntrsumbnd2  27077  pntleml  27121  tgcgrextend  27774  tgbtwnexch2  27785  tgifscgr  27797  tgcolg  27843  tgidinside  27860  tgbtwnconn1lem2  27862  tgbtwnconn1lem3  27863  lnhl  27904  tglinethru  27925  tglnpt2  27930  tglineneq  27933  coltr  27936  coltr3  27937  colline  27938  mirreu3  27943  miriso  27959  mirln  27965  mirln2  27966  mirconn  27967  mirbtwnhl  27969  colmid  27977  krippenlem  27979  midexlem  27981  ragflat  27993  ragcgr  27996  perprag  28015  perpdragALT  28016  colperpexlem1  28019  colperpexlem3  28021  midex  28026  opphllem1  28036  opphllem2  28037  opphllem5  28040  opphllem6  28041  hlpasch  28045  lmiisolem  28085  hypcgrlem1  28088  hypcgrlem2  28089  cgrg3col4  28142  upgrex  28390  crctcshwlk  29114  crctcsh  29116  1wlkdlem2  29429  eupth2lem3lem3  29521  eupth2lem3lem7  29525  nmcoplbi  31319  nmophmi  31322  nmbdfnlbi  31340  disjdifprg  31844  imadifxp  31870  2ndimaxp  31910  mptiffisupp  31953  xlt2addrd  32009  ssnnssfz  32036  gsumpart  32248  symgcntz  32287  pmtridf1o  32294  pmtridfv1  32295  pmtridfv2  32296  psgnfzto1stlem  32300  tocycf  32317  cycpmco2lem5  32330  cycpmco2  32333  dvdsruasso  32535  linds2eq  32542  ply1degltel  32711  ply1degleel  32712  ig1pmindeg  32718  locfinref  32890  zarcmplem  32930  esumpr2  33134  unelldsys  33225  sigapildsyslem  33228  sigapildsys  33229  mbfmcst  33327  carsgsigalem  33383  carsgclctunlem3  33388  pmeasmono  33392  probun  33487  0rrv  33519  sgncl  33606  signsvtn0  33650  signstfvneq0  33652  fineqvac  34166  btwnconn1lem11  35144  finxp00  36375  matunitlindf  36578  poimirlem14  36594  mblfinlem1  36617  mblfinlem2  36618  ismblfin  36621  itg2addnclem  36631  itgaddnclem2  36639  areacirclem4  36671  areacirc  36673  isbnd3  36744  blbnd  36747  rrnequiv  36795  lsmsat  37970  lkrscss  38060  eqlkr  38061  lkrshpor  38069  atcvrj2b  38395  atltcvr  38398  3dim1  38430  3dim2  38431  3dim3  38432  ps-2  38441  2at0mat0  38488  dalemdnee  38629  dalem63  38698  lnatexN  38742  2llnma3r  38751  pmodlem1  38809  pmapjat1  38816  pclfinclN  38913  osumclN  38930  pexmidALTN  38941  lhpexle2lem  38972  lhpexle3lem  38974  4atexlemex6  39037  4atex  39039  trlnle  39149  trlval3  39150  cdlemc  39160  cdlemd9  39169  cdleme27N  39332  cdleme28c  39335  cdleme32fvaw  39402  cdleme42ke  39448  cdleme42keg  39449  cdleme42mgN  39451  cdleme17d  39461  cdleme48fvg  39463  cdleme50trn123  39517  cdlemb3  39569  cdlemg8  39594  cdlemg15a  39618  cdlemg15  39619  cdlemg16  39620  cdlemg16ALTN  39621  cdlemg16z  39622  cdlemg16zz  39623  cdlemg20  39648  cdlemg22  39650  cdlemg37  39652  cdlemg31d  39663  cdlemg39  39679  cdlemg40  39680  ltrncom  39701  tendotr  39793  cdlemk25-3  39867  cdlemk35s-id  39901  cdlemk39s-id  39903  cdlemk53b  39919  cdlemk53  39920  cdlemk55  39924  cdlemk35u  39927  cdlemk55u  39929  cdlemk39u  39931  cdlemk19u  39933  cdleml5N  39943  dia2dimlem7  40033  dia2dimlem13  40039  dih1dimatlem  40292  dihlsprn  40294  dihjat1lem  40391  dihjat1  40392  dvh2dim  40408  dochexmid  40431  lclkrlem1  40469  lclkrlem2i  40478  lclkrlem2t  40489  lcfrlem34  40539  lcfrlem38  40543  lcfrlem41  40546  mapdindp1  40683  mapdindp2  40684  mapdh6dN  40702  mapdh6jN  40708  mapdh8j  40750  mapdh8  40751  hdmap1l6d  40776  hdmap1l6j  40782  hdmap11lem2  40805  hdmap14lem7  40837  jm2.19  41820  jm2.23  41823  nzss  43164  disjxp1  43844  cnrefiisplem  44630  xlimliminflimsup  44663  stoweidlem58  44859  fourierdlem41  44949  fourierdlem48  44955  fouriersw  45032  etransclem24  45059  nnfoctbdjlem  45256  smfpimltxr  45548  smfpimgtxr  45581  ssnn0ssfz  47110  mreclat  47706