Theorem pm2.61dane 3019

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ≠ wne 2932

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 207  df-an 396  df-ne 2933

This theorem is referenced by:  pm2.61da2ne  3020  pm2.61da3ne  3021  pm2.61iine  3022  disjxiun  5082  onfr  6362  f1oprswap  6825  soex  7872  frxp2  8094  frxp3  8101  riiner  8737  difsnen  8997  mapdom2  9086  nnunifi  9201  fofinf1o  9242  brwdom2  9488  cantnff  9595  cantnfp1  9602  carddomi2  9894  wdomfil  9983  fin1a2lem10  10331  fin1a2lem11  10332  uzsupss  12890  xaddcom  13192  xnegdi  13200  xpncan  13203  xleadd1a  13205  xsubge0  13213  ccat1st1st  14591  swrdccatin1  14687  cnpart  15202  fsumcllem  15694  fsumrev2  15744  expcnv  15829  geomulcvg  15841  fprodcllem  15916  fsumdvds  16277  gcd0id  16488  nn0seqcvgd  16539  lcmdvds  16577  mulgcddvds  16624  pcge0  16833  pcneg  16845  pcdvdstr  16847  pcz  16852  pcprmpw2  16853  pcadd  16860  ramcl2  16987  0ramcl  16994  ramub1lem1  16997  ramcl  17000  mrerintcl  17559  mreriincl  17560  mreexexlem4d  17613  mreclatBAD  18529  chnub  18588  psgnunilem1  19468  odmulg  19531  sylow1lem1  19573  pgpfi  19580  odadd1  19823  odadd2  19824  gsumval3  19882  gsumpt  19937  dprdfcntz  19992  dprd2da  20019  ablfac1eulem  20049  pgpfaclem3  20060  ablsimpgfind  20087  abvneg  20803  lssssr  20949  lspsneq  21120  lspdisj2  21125  drngnidl  21241  cnsubrg  21407  riinopn  22873  riincld  23009  neipeltop  23094  hauscmplem  23371  cmpfi  23373  ptbasfi  23546  xkoccn  23584  txindislem  23598  txtube  23605  hmphindis  23762  fclscmp  23995  utop2nei  24215  nrginvrcn  24657  nmoleub  24696  blcvx  24763  xrsxmet  24775  xrsblre  24777  lebnumlem3  24930  cphsqrtcl2  25153  ovollb2  25456  ioorcl  25544  i1fmulc  25670  itg1mulc  25671  mbfi1fseqlem4  25685  bddiblnc  25809  dvlip  25960  dvne0  25978  ig1pdvds  26145  plyeq0lem  26175  plyeq0  26176  aannenlem2  26295  aalioulem6  26303  abelthlem8  26404  abelth  26406  cxpexp  26632  cxpge0  26647  cxpmul2  26653  abscxp2  26657  abscxpbnd  26717  cxpeq  26721  nnlogbexp  26745  isosctrlem2  26783  atanrecl  26875  wilthlem2  27032  dchrabs2  27225  dchr1re  27226  lgsneg1  27285  lgsdirprm  27294  lgsdir  27295  lgsne0  27298  lgsdirnn0  27307  lgsdinn0  27308  2sqlem9  27390  rpvmasumlem  27450  dchrvmasumiflem1  27464  dchrisum0flblem1  27471  rpvmasum2  27475  pntrsumbnd2  27530  pntleml  27574  tgcgrextend  28553  tgbtwnexch2  28564  tgifscgr  28576  tgcolg  28622  tgidinside  28639  tgbtwnconn1lem2  28641  tgbtwnconn1lem3  28642  lnhl  28683  tglinethru  28704  tglnpt2  28709  tglineneq  28712  coltr  28715  coltr3  28716  colline  28717  mirreu3  28722  miriso  28738  mirln  28744  mirln2  28745  mirconn  28746  mirbtwnhl  28748  colmid  28756  krippenlem  28758  midexlem  28760  ragflat  28772  ragcgr  28775  perprag  28794  perpdragALT  28795  colperpexlem1  28798  colperpexlem3  28800  midex  28805  opphllem1  28815  opphllem2  28816  opphllem5  28819  opphllem6  28820  hlpasch  28824  lmiisolem  28864  hypcgrlem1  28867  hypcgrlem2  28868  cgrg3col4  28921  upgrex  29161  crctcshwlk  29890  crctcsh  29892  1wlkdlem2  30208  eupth2lem3lem3  30300  eupth2lem3lem7  30304  nmcoplbi  32099  nmophmi  32102  nmbdfnlbi  32120  disjdifprg  32645  imadifxp  32671  2ndimaxp  32719  mptiffisupp  32766  xlt2addrd  32832  ssnnssfz  32860  sgncl  32904  gsumpart  33124  suppgsumssiun  33133  symgcntz  33146  fzo0pmtrlast  33153  pmtridf1o  33155  pmtridfv1  33156  pmtridfv2  33157  psgnfzto1stlem  33161  tocycf  33178  cycpmco2lem5  33191  cycpmco2  33194  fxpgaval  33228  linds2eq  33441  dvdsruasso  33445  ply1coedeg  33649  ply1degltel  33654  ply1degleel  33655  ig1pmindeg  33662  esplyind  33719  fldext2chn  33872  constraddcl  33906  constrremulcl  33911  constrsqrtcl  33923  cos9thpiminplylem2  33927  locfinref  33985  zarcmplem  34025  esumpr2  34211  unelldsys  34302  sigapildsyslem  34305  sigapildsys  34306  mbfmcst  34403  carsgsigalem  34459  carsgclctunlem3  34464  pmeasmono  34468  probun  34563  0rrv  34595  signsvtn0  34714  signstfvneq0  34716  fineqvac  35260  wevgblacfn  35291  btwnconn1lem11  36279  finxp00  37718  matunitlindf  37939  poimirlem14  37955  mblfinlem1  37978  mblfinlem2  37979  ismblfin  37982  itg2addnclem  37992  itgaddnclem2  38000  areacirclem4  38032  areacirc  38034  isbnd3  38105  blbnd  38108  rrnequiv  38156  lsmsat  39454  lkrscss  39544  eqlkr  39545  lkrshpor  39553  atcvrj2b  39878  atltcvr  39881  3dim1  39913  3dim2  39914  3dim3  39915  ps-2  39924  2at0mat0  39971  dalemdnee  40112  dalem63  40181  lnatexN  40225  2llnma3r  40234  pmodlem1  40292  pmapjat1  40299  pclfinclN  40396  osumclN  40413  pexmidALTN  40424  lhpexle2lem  40455  lhpexle3lem  40457  4atexlemex6  40520  4atex  40522  trlnle  40632  trlval3  40633  cdlemc  40643  cdlemd9  40652  cdleme27N  40815  cdleme28c  40818  cdleme32fvaw  40885  cdleme42ke  40931  cdleme42keg  40932  cdleme42mgN  40934  cdleme17d  40944  cdleme48fvg  40946  cdleme50trn123  41000  cdlemb3  41052  cdlemg8  41077  cdlemg15a  41101  cdlemg15  41102  cdlemg16  41103  cdlemg16ALTN  41104  cdlemg16z  41105  cdlemg16zz  41106  cdlemg20  41131  cdlemg22  41133  cdlemg37  41135  cdlemg31d  41146  cdlemg39  41162  cdlemg40  41163  ltrncom  41184  tendotr  41276  cdlemk25-3  41350  cdlemk35s-id  41384  cdlemk39s-id  41386  cdlemk53b  41402  cdlemk53  41403  cdlemk55  41407  cdlemk35u  41410  cdlemk55u  41412  cdlemk39u  41414  cdlemk19u  41416  cdleml5N  41426  dia2dimlem7  41516  dia2dimlem13  41522  dih1dimatlem  41775  dihlsprn  41777  dihjat1lem  41874  dihjat1  41875  dvh2dim  41891  dochexmid  41914  lclkrlem1  41952  lclkrlem2i  41961  lclkrlem2t  41972  lcfrlem34  42022  lcfrlem38  42026  lcfrlem41  42029  mapdindp1  42166  mapdindp2  42167  mapdh6dN  42185  mapdh6jN  42191  mapdh8j  42233  mapdh8  42234  hdmap1l6d  42259  hdmap1l6j  42265  hdmap11lem2  42288  hdmap14lem7  42320  primrootlekpowne0  42544  aks6d1c7lem2  42620  unitscyglem4  42637  jm2.19  43421  jm2.23  43424  nzss  44744  disjxp1  45500  cnrefiisplem  46257  xlimliminflimsup  46290  stoweidlem58  46486  fourierdlem41  46576  fourierdlem48  46582  fouriersw  46659  etransclem24  46686  nnfoctbdjlem  46883  smfpimltxr  47175  smfpimgtxr  47208  chnerlem1  47312  ssnn0ssfz  48825  mreclat  49472