Theorem pm2.61dane 3028

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ≠ wne 2939

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 2940

This theorem is referenced by:  pm2.61da2ne  3029  pm2.61da3ne  3030  pm2.61iine  3031  disjxiun  5107  onfr  6361  f1oprswap  6833  soex  7863  frxp2  8081  frxp3  8088  riiner  8736  difsnen  9004  mapdom2  9099  nnunifi  9245  fofinf1o  9278  brwdom2  9518  cantnff  9619  cantnfp1  9626  carddomi2  9915  wdomfil  10006  fin1a2lem10  10354  fin1a2lem11  10355  uzsupss  12874  xaddcom  13169  xnegdi  13177  xpncan  13180  xleadd1a  13182  xsubge0  13190  ccat1st1st  14528  swrdccatin1  14625  cnpart  15137  fsumcllem  15628  fsumrev2  15678  expcnv  15760  geomulcvg  15772  fprodcllem  15845  fsumdvds  16201  gcd0id  16410  nn0seqcvgd  16457  lcmdvds  16495  mulgcddvds  16542  pcge0  16745  pcneg  16757  pcdvdstr  16759  pcz  16764  pcprmpw2  16765  pcadd  16772  ramcl2  16899  0ramcl  16906  ramub1lem1  16909  ramcl  16912  mrerintcl  17491  mreriincl  17492  mreexexlem4d  17541  mreclatBAD  18466  psgnunilem1  19289  odmulg  19352  sylow1lem1  19394  pgpfi  19401  odadd1  19640  odadd2  19641  gsumval3  19698  gsumpt  19753  dprdfcntz  19808  dprd2da  19835  ablfac1eulem  19865  pgpfaclem3  19876  ablsimpgfind  19903  abvneg  20349  lssssr  20471  lspsneq  20642  lspdisj2  20647  drngnidl  20758  cnsubrg  20894  riinopn  22294  riincld  22432  neipeltop  22517  hauscmplem  22794  cmpfi  22796  ptbasfi  22969  xkoccn  23007  txindislem  23021  txtube  23028  hmphindis  23185  fclscmp  23418  utop2nei  23639  nrginvrcn  24093  nmoleub  24132  blcvx  24198  xrsxmet  24209  xrsblre  24211  lebnumlem3  24363  cphsqrtcl2  24587  ovollb2  24890  ioorcl  24978  i1fmulc  25105  itg1mulc  25106  mbfi1fseqlem4  25120  bddiblnc  25243  dvlip  25394  dvne0  25412  ig1pdvds  25578  plyeq0lem  25608  plyeq0  25609  aannenlem2  25726  aalioulem6  25734  abelthlem8  25835  abelth  25837  cxpexp  26060  cxpge0  26075  cxpmul2  26081  abscxp2  26085  abscxpbnd  26143  cxpeq  26147  nnlogbexp  26168  isosctrlem2  26206  atanrecl  26298  wilthlem2  26455  dchrabs2  26647  dchr1re  26648  lgsneg1  26707  lgsdirprm  26716  lgsdir  26717  lgsne0  26720  lgsdirnn0  26729  lgsdinn0  26730  2sqlem9  26812  rpvmasumlem  26872  dchrvmasumiflem1  26886  dchrisum0flblem1  26893  rpvmasum2  26897  pntrsumbnd2  26952  pntleml  26996  tgcgrextend  27490  tgbtwnexch2  27501  tgifscgr  27513  tgcolg  27559  tgidinside  27576  tgbtwnconn1lem2  27578  tgbtwnconn1lem3  27579  lnhl  27620  tglinethru  27641  tglnpt2  27646  tglineneq  27649  coltr  27652  coltr3  27653  colline  27654  mirreu3  27659  miriso  27675  mirln  27681  mirln2  27682  mirconn  27683  mirbtwnhl  27685  colmid  27693  krippenlem  27695  midexlem  27697  ragflat  27709  ragcgr  27712  perprag  27731  perpdragALT  27732  colperpexlem1  27735  colperpexlem3  27737  midex  27742  opphllem1  27752  opphllem2  27753  opphllem5  27756  opphllem6  27757  hlpasch  27761  lmiisolem  27801  hypcgrlem1  27804  hypcgrlem2  27805  cgrg3col4  27858  upgrex  28106  crctcshwlk  28830  crctcsh  28832  1wlkdlem2  29145  eupth2lem3lem3  29237  eupth2lem3lem7  29241  nmcoplbi  31033  nmophmi  31036  nmbdfnlbi  31054  disjdifprg  31560  imadifxp  31586  2ndimaxp  31630  mptiffisupp  31675  xlt2addrd  31731  ssnnssfz  31758  gsumpart  31967  symgcntz  32006  pmtridf1o  32013  pmtridfv1  32014  pmtridfv2  32015  psgnfzto1stlem  32019  tocycf  32036  cycpmco2lem5  32049  cycpmco2  32052  linds2eq  32241  ply1degltel  32365  locfinref  32511  zarcmplem  32551  esumpr2  32755  unelldsys  32846  sigapildsyslem  32849  sigapildsys  32850  mbfmcst  32948  carsgsigalem  33004  carsgclctunlem3  33009  pmeasmono  33013  probun  33108  0rrv  33140  sgncl  33227  signsvtn0  33271  signstfvneq0  33273  fineqvac  33787  btwnconn1lem11  34758  finxp00  35946  matunitlindf  36149  poimirlem14  36165  mblfinlem1  36188  mblfinlem2  36189  ismblfin  36192  itg2addnclem  36202  itgaddnclem2  36210  areacirclem4  36242  areacirc  36244  isbnd3  36316  blbnd  36319  rrnequiv  36367  lsmsat  37543  lkrscss  37633  eqlkr  37634  lkrshpor  37642  atcvrj2b  37968  atltcvr  37971  3dim1  38003  3dim2  38004  3dim3  38005  ps-2  38014  2at0mat0  38061  dalemdnee  38202  dalem63  38271  lnatexN  38315  2llnma3r  38324  pmodlem1  38382  pmapjat1  38389  pclfinclN  38486  osumclN  38503  pexmidALTN  38514  lhpexle2lem  38545  lhpexle3lem  38547  4atexlemex6  38610  4atex  38612  trlnle  38722  trlval3  38723  cdlemc  38733  cdlemd9  38742  cdleme27N  38905  cdleme28c  38908  cdleme32fvaw  38975  cdleme42ke  39021  cdleme42keg  39022  cdleme42mgN  39024  cdleme17d  39034  cdleme48fvg  39036  cdleme50trn123  39090  cdlemb3  39142  cdlemg8  39167  cdlemg15a  39191  cdlemg15  39192  cdlemg16  39193  cdlemg16ALTN  39194  cdlemg16z  39195  cdlemg16zz  39196  cdlemg20  39221  cdlemg22  39223  cdlemg37  39225  cdlemg31d  39236  cdlemg39  39252  cdlemg40  39253  ltrncom  39274  tendotr  39366  cdlemk25-3  39440  cdlemk35s-id  39474  cdlemk39s-id  39476  cdlemk53b  39492  cdlemk53  39493  cdlemk55  39497  cdlemk35u  39500  cdlemk55u  39502  cdlemk39u  39504  cdlemk19u  39506  cdleml5N  39516  dia2dimlem7  39606  dia2dimlem13  39612  dih1dimatlem  39865  dihlsprn  39867  dihjat1lem  39964  dihjat1  39965  dvh2dim  39981  dochexmid  40004  lclkrlem1  40042  lclkrlem2i  40051  lclkrlem2t  40062  lcfrlem34  40112  lcfrlem38  40116  lcfrlem41  40119  mapdindp1  40256  mapdindp2  40257  mapdh6dN  40275  mapdh6jN  40281  mapdh8j  40323  mapdh8  40324  hdmap1l6d  40349  hdmap1l6j  40355  hdmap11lem2  40378  hdmap14lem7  40410  jm2.19  41375  jm2.23  41378  nzss  42719  disjxp1  43399  cnrefiisplem  44190  xlimliminflimsup  44223  stoweidlem58  44419  fourierdlem41  44509  fourierdlem48  44515  fouriersw  44592  etransclem24  44619  nnfoctbdjlem  44816  smfpimltxr  45108  smfpimgtxr  45141  ssnn0ssfz  46545  mreclat  47142