Theorem pm2.61dane 3030

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ≠ wne 2941

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 398  df-ne 2942

This theorem is referenced by:  pm2.61da2ne  3031  pm2.61da3ne  3032  pm2.61iine  3033  disjxiun  5146  onfr  6404  f1oprswap  6878  soex  7912  frxp2  8130  frxp3  8137  riiner  8784  difsnen  9053  mapdom2  9148  nnunifi  9294  fofinf1o  9327  brwdom2  9568  cantnff  9669  cantnfp1  9676  carddomi2  9965  wdomfil  10056  fin1a2lem10  10404  fin1a2lem11  10405  uzsupss  12924  xaddcom  13219  xnegdi  13227  xpncan  13230  xleadd1a  13232  xsubge0  13240  ccat1st1st  14578  swrdccatin1  14675  cnpart  15187  fsumcllem  15678  fsumrev2  15728  expcnv  15810  geomulcvg  15822  fprodcllem  15895  fsumdvds  16251  gcd0id  16460  nn0seqcvgd  16507  lcmdvds  16545  mulgcddvds  16592  pcge0  16795  pcneg  16807  pcdvdstr  16809  pcz  16814  pcprmpw2  16815  pcadd  16822  ramcl2  16949  0ramcl  16956  ramub1lem1  16959  ramcl  16962  mrerintcl  17541  mreriincl  17542  mreexexlem4d  17591  mreclatBAD  18516  psgnunilem1  19361  odmulg  19424  sylow1lem1  19466  pgpfi  19473  odadd1  19716  odadd2  19717  gsumval3  19775  gsumpt  19830  dprdfcntz  19885  dprd2da  19912  ablfac1eulem  19942  pgpfaclem3  19953  ablsimpgfind  19980  abvneg  20442  lssssr  20564  lspsneq  20735  lspdisj2  20740  drngnidl  20854  cnsubrg  21005  riinopn  22410  riincld  22548  neipeltop  22633  hauscmplem  22910  cmpfi  22912  ptbasfi  23085  xkoccn  23123  txindislem  23137  txtube  23144  hmphindis  23301  fclscmp  23534  utop2nei  23755  nrginvrcn  24209  nmoleub  24248  blcvx  24314  xrsxmet  24325  xrsblre  24327  lebnumlem3  24479  cphsqrtcl2  24703  ovollb2  25006  ioorcl  25094  i1fmulc  25221  itg1mulc  25222  mbfi1fseqlem4  25236  bddiblnc  25359  dvlip  25510  dvne0  25528  ig1pdvds  25694  plyeq0lem  25724  plyeq0  25725  aannenlem2  25842  aalioulem6  25850  abelthlem8  25951  abelth  25953  cxpexp  26176  cxpge0  26191  cxpmul2  26197  abscxp2  26201  abscxpbnd  26261  cxpeq  26265  nnlogbexp  26286  isosctrlem2  26324  atanrecl  26416  wilthlem2  26573  dchrabs2  26765  dchr1re  26766  lgsneg1  26825  lgsdirprm  26834  lgsdir  26835  lgsne0  26838  lgsdirnn0  26847  lgsdinn0  26848  2sqlem9  26930  rpvmasumlem  26990  dchrvmasumiflem1  27004  dchrisum0flblem1  27011  rpvmasum2  27015  pntrsumbnd2  27070  pntleml  27114  tgcgrextend  27736  tgbtwnexch2  27747  tgifscgr  27759  tgcolg  27805  tgidinside  27822  tgbtwnconn1lem2  27824  tgbtwnconn1lem3  27825  lnhl  27866  tglinethru  27887  tglnpt2  27892  tglineneq  27895  coltr  27898  coltr3  27899  colline  27900  mirreu3  27905  miriso  27921  mirln  27927  mirln2  27928  mirconn  27929  mirbtwnhl  27931  colmid  27939  krippenlem  27941  midexlem  27943  ragflat  27955  ragcgr  27958  perprag  27977  perpdragALT  27978  colperpexlem1  27981  colperpexlem3  27983  midex  27988  opphllem1  27998  opphllem2  27999  opphllem5  28002  opphllem6  28003  hlpasch  28007  lmiisolem  28047  hypcgrlem1  28050  hypcgrlem2  28051  cgrg3col4  28104  upgrex  28352  crctcshwlk  29076  crctcsh  29078  1wlkdlem2  29391  eupth2lem3lem3  29483  eupth2lem3lem7  29487  nmcoplbi  31281  nmophmi  31284  nmbdfnlbi  31302  disjdifprg  31806  imadifxp  31832  2ndimaxp  31872  mptiffisupp  31915  xlt2addrd  31971  ssnnssfz  31998  gsumpart  32207  symgcntz  32246  pmtridf1o  32253  pmtridfv1  32254  pmtridfv2  32255  psgnfzto1stlem  32259  tocycf  32276  cycpmco2lem5  32289  cycpmco2  32292  dvdsruasso  32490  linds2eq  32497  ply1degltel  32666  ig1pmindeg  32671  locfinref  32821  zarcmplem  32861  esumpr2  33065  unelldsys  33156  sigapildsyslem  33159  sigapildsys  33160  mbfmcst  33258  carsgsigalem  33314  carsgclctunlem3  33319  pmeasmono  33323  probun  33418  0rrv  33450  sgncl  33537  signsvtn0  33581  signstfvneq0  33583  fineqvac  34097  btwnconn1lem11  35069  finxp00  36283  matunitlindf  36486  poimirlem14  36502  mblfinlem1  36525  mblfinlem2  36526  ismblfin  36529  itg2addnclem  36539  itgaddnclem2  36547  areacirclem4  36579  areacirc  36581  isbnd3  36652  blbnd  36655  rrnequiv  36703  lsmsat  37878  lkrscss  37968  eqlkr  37969  lkrshpor  37977  atcvrj2b  38303  atltcvr  38306  3dim1  38338  3dim2  38339  3dim3  38340  ps-2  38349  2at0mat0  38396  dalemdnee  38537  dalem63  38606  lnatexN  38650  2llnma3r  38659  pmodlem1  38717  pmapjat1  38724  pclfinclN  38821  osumclN  38838  pexmidALTN  38849  lhpexle2lem  38880  lhpexle3lem  38882  4atexlemex6  38945  4atex  38947  trlnle  39057  trlval3  39058  cdlemc  39068  cdlemd9  39077  cdleme27N  39240  cdleme28c  39243  cdleme32fvaw  39310  cdleme42ke  39356  cdleme42keg  39357  cdleme42mgN  39359  cdleme17d  39369  cdleme48fvg  39371  cdleme50trn123  39425  cdlemb3  39477  cdlemg8  39502  cdlemg15a  39526  cdlemg15  39527  cdlemg16  39528  cdlemg16ALTN  39529  cdlemg16z  39530  cdlemg16zz  39531  cdlemg20  39556  cdlemg22  39558  cdlemg37  39560  cdlemg31d  39571  cdlemg39  39587  cdlemg40  39588  ltrncom  39609  tendotr  39701  cdlemk25-3  39775  cdlemk35s-id  39809  cdlemk39s-id  39811  cdlemk53b  39827  cdlemk53  39828  cdlemk55  39832  cdlemk35u  39835  cdlemk55u  39837  cdlemk39u  39839  cdlemk19u  39841  cdleml5N  39851  dia2dimlem7  39941  dia2dimlem13  39947  dih1dimatlem  40200  dihlsprn  40202  dihjat1lem  40299  dihjat1  40300  dvh2dim  40316  dochexmid  40339  lclkrlem1  40377  lclkrlem2i  40386  lclkrlem2t  40397  lcfrlem34  40447  lcfrlem38  40451  lcfrlem41  40454  mapdindp1  40591  mapdindp2  40592  mapdh6dN  40610  mapdh6jN  40616  mapdh8j  40658  mapdh8  40659  hdmap1l6d  40684  hdmap1l6j  40690  hdmap11lem2  40713  hdmap14lem7  40745  jm2.19  41732  jm2.23  41735  nzss  43076  disjxp1  43756  cnrefiisplem  44545  xlimliminflimsup  44578  stoweidlem58  44774  fourierdlem41  44864  fourierdlem48  44870  fouriersw  44947  etransclem24  44974  nnfoctbdjlem  45171  smfpimltxr  45463  smfpimgtxr  45496  ssnn0ssfz  47025  mreclat  47622