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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543   ≠ 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 210  df-an 400  df-ne 2941

This theorem is referenced by:  pm2.61da2ne  3030  pm2.61da3ne  3031  pm2.61iine  3032  disjxiun  5050  onfr  6252  f1oprswap  6704  soex  7699  riiner  8472  difsnen  8727  mapdom2  8817  nnunifi  8922  fofinf1o  8951  brwdom2  9189  cantnff  9289  cantnfp1  9296  carddomi2  9586  wdomfil  9675  fin1a2lem10  10023  fin1a2lem11  10024  uzsupss  12536  xaddcom  12830  xnegdi  12838  xpncan  12841  xleadd1a  12843  xsubge0  12851  ccat1st1st  14187  swrdccatin1  14290  cnpart  14803  fsumcllem  15296  fsumrev2  15346  expcnv  15428  geomulcvg  15440  fprodcllem  15513  fsumdvds  15869  gcd0id  16078  nn0seqcvgd  16127  lcmdvds  16165  mulgcddvds  16212  pcge0  16415  pcneg  16427  pcdvdstr  16429  pcz  16434  pcprmpw2  16435  pcadd  16442  ramcl2  16569  0ramcl  16576  ramub1lem1  16579  ramcl  16582  mrerintcl  17100  mreriincl  17101  mreexexlem4d  17150  mreclatBAD  18069  psgnunilem1  18885  odmulg  18947  sylow1lem1  18987  pgpfi  18994  odadd1  19233  odadd2  19234  gsumval3  19292  gsumpt  19347  dprdfcntz  19402  dprd2da  19429  ablfac1eulem  19459  pgpfaclem3  19470  ablsimpgfind  19497  abvneg  19870  lssssr  19990  lspsneq  20159  lspdisj2  20164  drngnidl  20267  cnsubrg  20423  riinopn  21805  riincld  21941  neipeltop  22026  hauscmplem  22303  cmpfi  22305  ptbasfi  22478  xkoccn  22516  txindislem  22530  txtube  22537  hmphindis  22694  fclscmp  22927  utop2nei  23148  nrginvrcn  23590  nmoleub  23629  blcvx  23695  xrsxmet  23706  xrsblre  23708  lebnumlem3  23860  cphsqrtcl2  24083  ovollb2  24386  ioorcl  24474  i1fmulc  24601  itg1mulc  24602  mbfi1fseqlem4  24616  bddiblnc  24739  dvlip  24890  dvne0  24908  ig1pdvds  25074  plyeq0lem  25104  plyeq0  25105  aannenlem2  25222  aalioulem6  25230  abelthlem8  25331  abelth  25333  cxpexp  25556  cxpge0  25571  cxpmul2  25577  abscxp2  25581  abscxpbnd  25639  cxpeq  25643  nnlogbexp  25664  isosctrlem2  25702  atanrecl  25794  wilthlem2  25951  dchrabs2  26143  dchr1re  26144  lgsneg1  26203  lgsdirprm  26212  lgsdir  26213  lgsne0  26216  lgsdirnn0  26225  lgsdinn0  26226  2sqlem9  26308  rpvmasumlem  26368  dchrvmasumiflem1  26382  dchrisum0flblem1  26389  rpvmasum2  26393  pntrsumbnd2  26448  pntleml  26492  tgcgrextend  26576  tgbtwnexch2  26587  tgifscgr  26599  tgcolg  26645  tgidinside  26662  tgbtwnconn1lem2  26664  tgbtwnconn1lem3  26665  lnhl  26706  tglinethru  26727  tglnpt2  26732  tglineneq  26735  coltr  26738  coltr3  26739  colline  26740  mirreu3  26745  miriso  26761  mirln  26767  mirln2  26768  mirconn  26769  mirbtwnhl  26771  colmid  26779  krippenlem  26781  midexlem  26783  ragflat  26795  ragcgr  26798  perprag  26817  perpdragALT  26818  colperpexlem1  26821  colperpexlem3  26823  midex  26828  opphllem1  26838  opphllem2  26839  opphllem5  26842  opphllem6  26843  hlpasch  26847  lmiisolem  26887  hypcgrlem1  26890  hypcgrlem2  26891  cgrg3col4  26944  upgrex  27183  crctcshwlk  27906  crctcsh  27908  1wlkdlem2  28221  eupth2lem3lem3  28313  eupth2lem3lem7  28317  nmcoplbi  30109  nmophmi  30112  nmbdfnlbi  30130  disjdifprg  30633  imadifxp  30659  2ndimaxp  30703  xlt2addrd  30801  ssnnssfz  30828  gsumpart  31034  symgcntz  31073  pmtridf1o  31080  pmtridfv1  31081  pmtridfv2  31082  psgnfzto1stlem  31086  tocycf  31103  cycpmco2lem5  31116  cycpmco2  31119  linds2eq  31289  locfinref  31505  zarcmplem  31545  esumpr2  31747  unelldsys  31838  sigapildsyslem  31841  sigapildsys  31842  mbfmcst  31938  carsgsigalem  31994  carsgclctunlem3  31999  pmeasmono  32003  probun  32098  0rrv  32130  sgncl  32217  signsvtn0  32261  signstfvneq0  32263  fineqvac  32779  frxp2  33528  frxp3  33534  btwnconn1lem11  34136  finxp00  35310  matunitlindf  35512  poimirlem14  35528  mblfinlem1  35551  mblfinlem2  35552  ismblfin  35555  itg2addnclem  35565  itgaddnclem2  35573  areacirclem4  35605  areacirc  35607  isbnd3  35679  blbnd  35682  rrnequiv  35730  lsmsat  36759  lkrscss  36849  eqlkr  36850  lkrshpor  36858  atcvrj2b  37183  atltcvr  37186  3dim1  37218  3dim2  37219  3dim3  37220  ps-2  37229  2at0mat0  37276  dalemdnee  37417  dalem63  37486  lnatexN  37530  2llnma3r  37539  pmodlem1  37597  pmapjat1  37604  pclfinclN  37701  osumclN  37718  pexmidALTN  37729  lhpexle2lem  37760  lhpexle3lem  37762  4atexlemex6  37825  4atex  37827  trlnle  37937  trlval3  37938  cdlemc  37948  cdlemd9  37957  cdleme27N  38120  cdleme28c  38123  cdleme32fvaw  38190  cdleme42ke  38236  cdleme42keg  38237  cdleme42mgN  38239  cdleme17d  38249  cdleme48fvg  38251  cdleme50trn123  38305  cdlemb3  38357  cdlemg8  38382  cdlemg15a  38406  cdlemg15  38407  cdlemg16  38408  cdlemg16ALTN  38409  cdlemg16z  38410  cdlemg16zz  38411  cdlemg20  38436  cdlemg22  38438  cdlemg37  38440  cdlemg31d  38451  cdlemg39  38467  cdlemg40  38468  ltrncom  38489  tendotr  38581  cdlemk25-3  38655  cdlemk35s-id  38689  cdlemk39s-id  38691  cdlemk53b  38707  cdlemk53  38708  cdlemk55  38712  cdlemk35u  38715  cdlemk55u  38717  cdlemk39u  38719  cdlemk19u  38721  cdleml5N  38731  dia2dimlem7  38821  dia2dimlem13  38827  dih1dimatlem  39080  dihlsprn  39082  dihjat1lem  39179  dihjat1  39180  dvh2dim  39196  dochexmid  39219  lclkrlem1  39257  lclkrlem2i  39266  lclkrlem2t  39277  lcfrlem34  39327  lcfrlem38  39331  lcfrlem41  39334  mapdindp1  39471  mapdindp2  39472  mapdh6dN  39490  mapdh6jN  39496  mapdh8j  39538  mapdh8  39539  hdmap1l6d  39564  hdmap1l6j  39570  hdmap11lem2  39593  hdmap14lem7  39625  jm2.19  40518  jm2.23  40521  nzss  41608  disjxp1  42290  cnrefiisplem  43045  xlimliminflimsup  43078  stoweidlem58  43274  fourierdlem41  43364  fourierdlem48  43370  fouriersw  43447  etransclem24  43474  nnfoctbdjlem  43668  ssnn0ssfz  45358  mreclat  45956