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  5092  onfr  6350  f1oprswap  6812  soex  7861  frxp2  8084  frxp3  8091  riiner  8724  difsnen  8983  mapdom2  9072  nnunifi  9196  fofinf1o  9241  brwdom2  9484  cantnff  9589  cantnfp1  9596  carddomi2  9885  wdomfil  9974  fin1a2lem10  10322  fin1a2lem11  10323  uzsupss  12859  xaddcom  13160  xnegdi  13168  xpncan  13171  xleadd1a  13173  xsubge0  13181  ccat1st1st  14553  swrdccatin1  14649  cnpart  15165  fsumcllem  15657  fsumrev2  15707  expcnv  15789  geomulcvg  15801  fprodcllem  15876  fsumdvds  16237  gcd0id  16448  nn0seqcvgd  16499  lcmdvds  16537  mulgcddvds  16584  pcge0  16792  pcneg  16804  pcdvdstr  16806  pcz  16811  pcprmpw2  16812  pcadd  16819  ramcl2  16946  0ramcl  16953  ramub1lem1  16956  ramcl  16959  mrerintcl  17517  mreriincl  17518  mreexexlem4d  17571  mreclatBAD  18487  psgnunilem1  19390  odmulg  19453  sylow1lem1  19495  pgpfi  19502  odadd1  19745  odadd2  19746  gsumval3  19804  gsumpt  19859  dprdfcntz  19914  dprd2da  19941  ablfac1eulem  19971  pgpfaclem3  19982  ablsimpgfind  20009  abvneg  20729  lssssr  20875  lspsneq  21047  lspdisj2  21052  drngnidl  21168  cnsubrg  21352  riinopn  22811  riincld  22947  neipeltop  23032  hauscmplem  23309  cmpfi  23311  ptbasfi  23484  xkoccn  23522  txindislem  23536  txtube  23543  hmphindis  23700  fclscmp  23933  utop2nei  24154  nrginvrcn  24596  nmoleub  24635  blcvx  24702  xrsxmet  24714  xrsblre  24716  lebnumlem3  24878  cphsqrtcl2  25102  ovollb2  25406  ioorcl  25494  i1fmulc  25620  itg1mulc  25621  mbfi1fseqlem4  25635  bddiblnc  25759  dvlip  25914  dvne0  25932  ig1pdvds  26101  plyeq0lem  26131  plyeq0  26132  aannenlem2  26253  aalioulem6  26261  abelthlem8  26365  abelth  26367  cxpexp  26593  cxpge0  26608  cxpmul2  26614  abscxp2  26618  abscxpbnd  26679  cxpeq  26683  nnlogbexp  26707  isosctrlem2  26745  atanrecl  26837  wilthlem2  26995  dchrabs2  27189  dchr1re  27190  lgsneg1  27249  lgsdirprm  27258  lgsdir  27259  lgsne0  27262  lgsdirnn0  27271  lgsdinn0  27272  2sqlem9  27354  rpvmasumlem  27414  dchrvmasumiflem1  27428  dchrisum0flblem1  27435  rpvmasum2  27439  pntrsumbnd2  27494  pntleml  27538  tgcgrextend  28448  tgbtwnexch2  28459  tgifscgr  28471  tgcolg  28517  tgidinside  28534  tgbtwnconn1lem2  28536  tgbtwnconn1lem3  28537  lnhl  28578  tglinethru  28599  tglnpt2  28604  tglineneq  28607  coltr  28610  coltr3  28611  colline  28612  mirreu3  28617  miriso  28633  mirln  28639  mirln2  28640  mirconn  28641  mirbtwnhl  28643  colmid  28651  krippenlem  28653  midexlem  28655  ragflat  28667  ragcgr  28670  perprag  28689  perpdragALT  28690  colperpexlem1  28693  colperpexlem3  28695  midex  28700  opphllem1  28710  opphllem2  28711  opphllem5  28714  opphllem6  28715  hlpasch  28719  lmiisolem  28759  hypcgrlem1  28762  hypcgrlem2  28763  cgrg3col4  28816  upgrex  29055  crctcshwlk  29785  crctcsh  29787  1wlkdlem2  30100  eupth2lem3lem3  30192  eupth2lem3lem7  30196  nmcoplbi  31990  nmophmi  31993  nmbdfnlbi  32011  disjdifprg  32537  imadifxp  32563  2ndimaxp  32603  mptiffisupp  32649  xlt2addrd  32715  ssnnssfz  32743  sgncl  32789  chnub  32967  gsumpart  33023  symgcntz  33040  fzo0pmtrlast  33047  pmtridf1o  33049  pmtridfv1  33050  pmtridfv2  33051  psgnfzto1stlem  33055  tocycf  33072  cycpmco2lem5  33085  cycpmco2  33088  fxpgaval  33122  linds2eq  33328  dvdsruasso  33332  ply1degltel  33536  ply1degleel  33537  ig1pmindeg  33543  fldext2chn  33694  constraddcl  33728  constrremulcl  33733  constrsqrtcl  33745  cos9thpiminplylem2  33749  locfinref  33807  zarcmplem  33847  esumpr2  34033  unelldsys  34124  sigapildsyslem  34127  sigapildsys  34128  mbfmcst  34226  carsgsigalem  34282  carsgclctunlem3  34287  pmeasmono  34291  probun  34386  0rrv  34418  signsvtn0  34537  signstfvneq0  34539  fineqvac  35071  wevgblacfn  35081  btwnconn1lem11  36070  finxp00  37375  matunitlindf  37597  poimirlem14  37613  mblfinlem1  37636  mblfinlem2  37637  ismblfin  37640  itg2addnclem  37650  itgaddnclem2  37658  areacirclem4  37690  areacirc  37692  isbnd3  37763  blbnd  37766  rrnequiv  37814  lsmsat  38986  lkrscss  39076  eqlkr  39077  lkrshpor  39085  atcvrj2b  39411  atltcvr  39414  3dim1  39446  3dim2  39447  3dim3  39448  ps-2  39457  2at0mat0  39504  dalemdnee  39645  dalem63  39714  lnatexN  39758  2llnma3r  39767  pmodlem1  39825  pmapjat1  39832  pclfinclN  39929  osumclN  39946  pexmidALTN  39957  lhpexle2lem  39988  lhpexle3lem  39990  4atexlemex6  40053  4atex  40055  trlnle  40165  trlval3  40166  cdlemc  40176  cdlemd9  40185  cdleme27N  40348  cdleme28c  40351  cdleme32fvaw  40418  cdleme42ke  40464  cdleme42keg  40465  cdleme42mgN  40467  cdleme17d  40477  cdleme48fvg  40479  cdleme50trn123  40533  cdlemb3  40585  cdlemg8  40610  cdlemg15a  40634  cdlemg15  40635  cdlemg16  40636  cdlemg16ALTN  40637  cdlemg16z  40638  cdlemg16zz  40639  cdlemg20  40664  cdlemg22  40666  cdlemg37  40668  cdlemg31d  40679  cdlemg39  40695  cdlemg40  40696  ltrncom  40717  tendotr  40809  cdlemk25-3  40883  cdlemk35s-id  40917  cdlemk39s-id  40919  cdlemk53b  40935  cdlemk53  40936  cdlemk55  40940  cdlemk35u  40943  cdlemk55u  40945  cdlemk39u  40947  cdlemk19u  40949  cdleml5N  40959  dia2dimlem7  41049  dia2dimlem13  41055  dih1dimatlem  41308  dihlsprn  41310  dihjat1lem  41407  dihjat1  41408  dvh2dim  41424  dochexmid  41447  lclkrlem1  41485  lclkrlem2i  41494  lclkrlem2t  41505  lcfrlem34  41555  lcfrlem38  41559  lcfrlem41  41562  mapdindp1  41699  mapdindp2  41700  mapdh6dN  41718  mapdh6jN  41724  mapdh8j  41766  mapdh8  41767  hdmap1l6d  41792  hdmap1l6j  41798  hdmap11lem2  41821  hdmap14lem7  41853  primrootlekpowne0  42078  aks6d1c7lem2  42154  unitscyglem4  42171  jm2.19  42966  jm2.23  42969  nzss  44290  disjxp1  45047  cnrefiisplem  45811  xlimliminflimsup  45844  stoweidlem58  46040  fourierdlem41  46130  fourierdlem48  46136  fouriersw  46213  etransclem24  46240  nnfoctbdjlem  46437  smfpimltxr  46729  smfpimgtxr  46762  ssnn0ssfz  48334  mreclat  48982