Theorem pm2.61dane 3016

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ≠ wne 2929

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 2930

This theorem is referenced by:  pm2.61da2ne  3017  pm2.61da3ne  3018  pm2.61iine  3019  disjxiun  5090  onfr  6350  f1oprswap  6813  soex  7857  frxp2  8080  frxp3  8087  riiner  8720  difsnen  8979  mapdom2  9068  nnunifi  9182  fofinf1o  9223  brwdom2  9466  cantnff  9571  cantnfp1  9578  carddomi2  9870  wdomfil  9959  fin1a2lem10  10307  fin1a2lem11  10308  uzsupss  12840  xaddcom  13141  xnegdi  13149  xpncan  13152  xleadd1a  13154  xsubge0  13162  ccat1st1st  14538  swrdccatin1  14634  cnpart  15149  fsumcllem  15641  fsumrev2  15691  expcnv  15773  geomulcvg  15785  fprodcllem  15860  fsumdvds  16221  gcd0id  16432  nn0seqcvgd  16483  lcmdvds  16521  mulgcddvds  16568  pcge0  16776  pcneg  16788  pcdvdstr  16790  pcz  16795  pcprmpw2  16796  pcadd  16803  ramcl2  16930  0ramcl  16937  ramub1lem1  16940  ramcl  16943  mrerintcl  17501  mreriincl  17502  mreexexlem4d  17555  mreclatBAD  18471  chnub  18530  psgnunilem1  19407  odmulg  19470  sylow1lem1  19512  pgpfi  19519  odadd1  19762  odadd2  19763  gsumval3  19821  gsumpt  19876  dprdfcntz  19931  dprd2da  19958  ablfac1eulem  19988  pgpfaclem3  19999  ablsimpgfind  20026  abvneg  20743  lssssr  20889  lspsneq  21061  lspdisj2  21066  drngnidl  21182  cnsubrg  21366  riinopn  22824  riincld  22960  neipeltop  23045  hauscmplem  23322  cmpfi  23324  ptbasfi  23497  xkoccn  23535  txindislem  23549  txtube  23556  hmphindis  23713  fclscmp  23946  utop2nei  24166  nrginvrcn  24608  nmoleub  24647  blcvx  24714  xrsxmet  24726  xrsblre  24728  lebnumlem3  24890  cphsqrtcl2  25114  ovollb2  25418  ioorcl  25506  i1fmulc  25632  itg1mulc  25633  mbfi1fseqlem4  25647  bddiblnc  25771  dvlip  25926  dvne0  25944  ig1pdvds  26113  plyeq0lem  26143  plyeq0  26144  aannenlem2  26265  aalioulem6  26273  abelthlem8  26377  abelth  26379  cxpexp  26605  cxpge0  26620  cxpmul2  26626  abscxp2  26630  abscxpbnd  26691  cxpeq  26695  nnlogbexp  26719  isosctrlem2  26757  atanrecl  26849  wilthlem2  27007  dchrabs2  27201  dchr1re  27202  lgsneg1  27261  lgsdirprm  27270  lgsdir  27271  lgsne0  27274  lgsdirnn0  27283  lgsdinn0  27284  2sqlem9  27366  rpvmasumlem  27426  dchrvmasumiflem1  27440  dchrisum0flblem1  27447  rpvmasum2  27451  pntrsumbnd2  27506  pntleml  27550  tgcgrextend  28464  tgbtwnexch2  28475  tgifscgr  28487  tgcolg  28533  tgidinside  28550  tgbtwnconn1lem2  28552  tgbtwnconn1lem3  28553  lnhl  28594  tglinethru  28615  tglnpt2  28620  tglineneq  28623  coltr  28626  coltr3  28627  colline  28628  mirreu3  28633  miriso  28649  mirln  28655  mirln2  28656  mirconn  28657  mirbtwnhl  28659  colmid  28667  krippenlem  28669  midexlem  28671  ragflat  28683  ragcgr  28686  perprag  28705  perpdragALT  28706  colperpexlem1  28709  colperpexlem3  28711  midex  28716  opphllem1  28726  opphllem2  28727  opphllem5  28730  opphllem6  28731  hlpasch  28735  lmiisolem  28775  hypcgrlem1  28778  hypcgrlem2  28779  cgrg3col4  28832  upgrex  29072  crctcshwlk  29802  crctcsh  29804  1wlkdlem2  30120  eupth2lem3lem3  30212  eupth2lem3lem7  30216  nmcoplbi  32010  nmophmi  32013  nmbdfnlbi  32031  disjdifprg  32557  imadifxp  32583  2ndimaxp  32630  mptiffisupp  32678  xlt2addrd  32746  ssnnssfz  32774  sgncl  32819  gsumpart  33044  symgcntz  33061  fzo0pmtrlast  33068  pmtridf1o  33070  pmtridfv1  33071  pmtridfv2  33072  psgnfzto1stlem  33076  tocycf  33093  cycpmco2lem5  33106  cycpmco2  33109  fxpgaval  33143  linds2eq  33353  dvdsruasso  33357  ply1degltel  33562  ply1degleel  33563  ig1pmindeg  33569  esplyind  33613  fldext2chn  33762  constraddcl  33796  constrremulcl  33801  constrsqrtcl  33813  cos9thpiminplylem2  33817  locfinref  33875  zarcmplem  33915  esumpr2  34101  unelldsys  34192  sigapildsyslem  34195  sigapildsys  34196  mbfmcst  34293  carsgsigalem  34349  carsgclctunlem3  34354  pmeasmono  34358  probun  34453  0rrv  34485  signsvtn0  34604  signstfvneq0  34606  fineqvac  35160  wevgblacfn  35174  btwnconn1lem11  36162  finxp00  37467  matunitlindf  37678  poimirlem14  37694  mblfinlem1  37717  mblfinlem2  37718  ismblfin  37721  itg2addnclem  37731  itgaddnclem2  37739  areacirclem4  37771  areacirc  37773  isbnd3  37844  blbnd  37847  rrnequiv  37895  lsmsat  39127  lkrscss  39217  eqlkr  39218  lkrshpor  39226  atcvrj2b  39551  atltcvr  39554  3dim1  39586  3dim2  39587  3dim3  39588  ps-2  39597  2at0mat0  39644  dalemdnee  39785  dalem63  39854  lnatexN  39898  2llnma3r  39907  pmodlem1  39965  pmapjat1  39972  pclfinclN  40069  osumclN  40086  pexmidALTN  40097  lhpexle2lem  40128  lhpexle3lem  40130  4atexlemex6  40193  4atex  40195  trlnle  40305  trlval3  40306  cdlemc  40316  cdlemd9  40325  cdleme27N  40488  cdleme28c  40491  cdleme32fvaw  40558  cdleme42ke  40604  cdleme42keg  40605  cdleme42mgN  40607  cdleme17d  40617  cdleme48fvg  40619  cdleme50trn123  40673  cdlemb3  40725  cdlemg8  40750  cdlemg15a  40774  cdlemg15  40775  cdlemg16  40776  cdlemg16ALTN  40777  cdlemg16z  40778  cdlemg16zz  40779  cdlemg20  40804  cdlemg22  40806  cdlemg37  40808  cdlemg31d  40819  cdlemg39  40835  cdlemg40  40836  ltrncom  40857  tendotr  40949  cdlemk25-3  41023  cdlemk35s-id  41057  cdlemk39s-id  41059  cdlemk53b  41075  cdlemk53  41076  cdlemk55  41080  cdlemk35u  41083  cdlemk55u  41085  cdlemk39u  41087  cdlemk19u  41089  cdleml5N  41099  dia2dimlem7  41189  dia2dimlem13  41195  dih1dimatlem  41448  dihlsprn  41450  dihjat1lem  41547  dihjat1  41548  dvh2dim  41564  dochexmid  41587  lclkrlem1  41625  lclkrlem2i  41634  lclkrlem2t  41645  lcfrlem34  41695  lcfrlem38  41699  lcfrlem41  41702  mapdindp1  41839  mapdindp2  41840  mapdh6dN  41858  mapdh6jN  41864  mapdh8j  41906  mapdh8  41907  hdmap1l6d  41932  hdmap1l6j  41938  hdmap11lem2  41961  hdmap14lem7  41993  primrootlekpowne0  42218  aks6d1c7lem2  42294  unitscyglem4  42311  jm2.19  43110  jm2.23  43113  nzss  44434  disjxp1  45190  cnrefiisplem  45951  xlimliminflimsup  45984  stoweidlem58  46180  fourierdlem41  46270  fourierdlem48  46276  fouriersw  46353  etransclem24  46380  nnfoctbdjlem  46577  smfpimltxr  46869  smfpimgtxr  46902  chnerlem1  47004  ssnn0ssfz  48473  mreclat  49121