Theorem pm2.61dane 3012

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 3011	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ≠ wne 2925

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 2926

This theorem is referenced by:  pm2.61da2ne  3013  pm2.61da3ne  3014  pm2.61iine  3015  disjxiun  5104  onfr  6371  f1oprswap  6844  soex  7897  frxp2  8123  frxp3  8130  riiner  8763  difsnen  9023  mapdom2  9112  nnunifi  9238  fofinf1o  9283  brwdom2  9526  cantnff  9627  cantnfp1  9634  carddomi2  9923  wdomfil  10014  fin1a2lem10  10362  fin1a2lem11  10363  uzsupss  12899  xaddcom  13200  xnegdi  13208  xpncan  13211  xleadd1a  13213  xsubge0  13221  ccat1st1st  14593  swrdccatin1  14690  cnpart  15206  fsumcllem  15698  fsumrev2  15748  expcnv  15830  geomulcvg  15842  fprodcllem  15917  fsumdvds  16278  gcd0id  16489  nn0seqcvgd  16540  lcmdvds  16578  mulgcddvds  16625  pcge0  16833  pcneg  16845  pcdvdstr  16847  pcz  16852  pcprmpw2  16853  pcadd  16860  ramcl2  16987  0ramcl  16994  ramub1lem1  16997  ramcl  17000  mrerintcl  17558  mreriincl  17559  mreexexlem4d  17608  mreclatBAD  18522  psgnunilem1  19423  odmulg  19486  sylow1lem1  19528  pgpfi  19535  odadd1  19778  odadd2  19779  gsumval3  19837  gsumpt  19892  dprdfcntz  19947  dprd2da  19974  ablfac1eulem  20004  pgpfaclem3  20015  ablsimpgfind  20042  abvneg  20735  lssssr  20860  lspsneq  21032  lspdisj2  21037  drngnidl  21153  cnsubrg  21344  riinopn  22795  riincld  22931  neipeltop  23016  hauscmplem  23293  cmpfi  23295  ptbasfi  23468  xkoccn  23506  txindislem  23520  txtube  23527  hmphindis  23684  fclscmp  23917  utop2nei  24138  nrginvrcn  24580  nmoleub  24619  blcvx  24686  xrsxmet  24698  xrsblre  24700  lebnumlem3  24862  cphsqrtcl2  25086  ovollb2  25390  ioorcl  25478  i1fmulc  25604  itg1mulc  25605  mbfi1fseqlem4  25619  bddiblnc  25743  dvlip  25898  dvne0  25916  ig1pdvds  26085  plyeq0lem  26115  plyeq0  26116  aannenlem2  26237  aalioulem6  26245  abelthlem8  26349  abelth  26351  cxpexp  26577  cxpge0  26592  cxpmul2  26598  abscxp2  26602  abscxpbnd  26663  cxpeq  26667  nnlogbexp  26691  isosctrlem2  26729  atanrecl  26821  wilthlem2  26979  dchrabs2  27173  dchr1re  27174  lgsneg1  27233  lgsdirprm  27242  lgsdir  27243  lgsne0  27246  lgsdirnn0  27255  lgsdinn0  27256  2sqlem9  27338  rpvmasumlem  27398  dchrvmasumiflem1  27412  dchrisum0flblem1  27419  rpvmasum2  27423  pntrsumbnd2  27478  pntleml  27522  tgcgrextend  28412  tgbtwnexch2  28423  tgifscgr  28435  tgcolg  28481  tgidinside  28498  tgbtwnconn1lem2  28500  tgbtwnconn1lem3  28501  lnhl  28542  tglinethru  28563  tglnpt2  28568  tglineneq  28571  coltr  28574  coltr3  28575  colline  28576  mirreu3  28581  miriso  28597  mirln  28603  mirln2  28604  mirconn  28605  mirbtwnhl  28607  colmid  28615  krippenlem  28617  midexlem  28619  ragflat  28631  ragcgr  28634  perprag  28653  perpdragALT  28654  colperpexlem1  28657  colperpexlem3  28659  midex  28664  opphllem1  28674  opphllem2  28675  opphllem5  28678  opphllem6  28679  hlpasch  28683  lmiisolem  28723  hypcgrlem1  28726  hypcgrlem2  28727  cgrg3col4  28780  upgrex  29019  crctcshwlk  29752  crctcsh  29754  1wlkdlem2  30067  eupth2lem3lem3  30159  eupth2lem3lem7  30163  nmcoplbi  31957  nmophmi  31960  nmbdfnlbi  31978  disjdifprg  32504  imadifxp  32530  2ndimaxp  32570  mptiffisupp  32616  xlt2addrd  32682  ssnnssfz  32710  sgncl  32756  chnub  32938  gsumpart  32997  symgcntz  33042  fzo0pmtrlast  33049  pmtridf1o  33051  pmtridfv1  33052  pmtridfv2  33053  psgnfzto1stlem  33057  tocycf  33074  cycpmco2lem5  33087  cycpmco2  33090  fxpgaval  33124  linds2eq  33352  dvdsruasso  33356  ply1degltel  33560  ply1degleel  33561  ig1pmindeg  33567  fldext2chn  33718  constraddcl  33752  constrremulcl  33757  constrsqrtcl  33769  cos9thpiminplylem2  33773  locfinref  33831  zarcmplem  33871  esumpr2  34057  unelldsys  34148  sigapildsyslem  34151  sigapildsys  34152  mbfmcst  34250  carsgsigalem  34306  carsgclctunlem3  34311  pmeasmono  34315  probun  34410  0rrv  34442  signsvtn0  34561  signstfvneq0  34563  fineqvac  35087  wevgblacfn  35096  btwnconn1lem11  36085  finxp00  37390  matunitlindf  37612  poimirlem14  37628  mblfinlem1  37651  mblfinlem2  37652  ismblfin  37655  itg2addnclem  37665  itgaddnclem2  37673  areacirclem4  37705  areacirc  37707  isbnd3  37778  blbnd  37781  rrnequiv  37829  lsmsat  39001  lkrscss  39091  eqlkr  39092  lkrshpor  39100  atcvrj2b  39426  atltcvr  39429  3dim1  39461  3dim2  39462  3dim3  39463  ps-2  39472  2at0mat0  39519  dalemdnee  39660  dalem63  39729  lnatexN  39773  2llnma3r  39782  pmodlem1  39840  pmapjat1  39847  pclfinclN  39944  osumclN  39961  pexmidALTN  39972  lhpexle2lem  40003  lhpexle3lem  40005  4atexlemex6  40068  4atex  40070  trlnle  40180  trlval3  40181  cdlemc  40191  cdlemd9  40200  cdleme27N  40363  cdleme28c  40366  cdleme32fvaw  40433  cdleme42ke  40479  cdleme42keg  40480  cdleme42mgN  40482  cdleme17d  40492  cdleme48fvg  40494  cdleme50trn123  40548  cdlemb3  40600  cdlemg8  40625  cdlemg15a  40649  cdlemg15  40650  cdlemg16  40651  cdlemg16ALTN  40652  cdlemg16z  40653  cdlemg16zz  40654  cdlemg20  40679  cdlemg22  40681  cdlemg37  40683  cdlemg31d  40694  cdlemg39  40710  cdlemg40  40711  ltrncom  40732  tendotr  40824  cdlemk25-3  40898  cdlemk35s-id  40932  cdlemk39s-id  40934  cdlemk53b  40950  cdlemk53  40951  cdlemk55  40955  cdlemk35u  40958  cdlemk55u  40960  cdlemk39u  40962  cdlemk19u  40964  cdleml5N  40974  dia2dimlem7  41064  dia2dimlem13  41070  dih1dimatlem  41323  dihlsprn  41325  dihjat1lem  41422  dihjat1  41423  dvh2dim  41439  dochexmid  41462  lclkrlem1  41500  lclkrlem2i  41509  lclkrlem2t  41520  lcfrlem34  41570  lcfrlem38  41574  lcfrlem41  41577  mapdindp1  41714  mapdindp2  41715  mapdh6dN  41733  mapdh6jN  41739  mapdh8j  41781  mapdh8  41782  hdmap1l6d  41807  hdmap1l6j  41813  hdmap11lem2  41836  hdmap14lem7  41868  primrootlekpowne0  42093  aks6d1c7lem2  42169  unitscyglem4  42186  jm2.19  42982  jm2.23  42985  nzss  44306  disjxp1  45063  cnrefiisplem  45827  xlimliminflimsup  45860  stoweidlem58  46056  fourierdlem41  46146  fourierdlem48  46152  fouriersw  46229  etransclem24  46256  nnfoctbdjlem  46453  smfpimltxr  46745  smfpimgtxr  46778  ssnn0ssfz  48337  mreclat  48985