Theorem pm2.61dane 3044

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ≠ wne 2957

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-ne 2958

This theorem is used by:  pm2.61da2ne  3045  pm2.61da3ne  3046  pm2.61iine  3047  disjxiun  5104  onfr  6401  f1oprswap  6867  soex  7922  frxp2  8146  frxp3  8153  riiner  8794  difsnen  9061  mapdom2  9150  nnunifi  9265  fofinf1o  9303  brwdom2  9549  cantnff  9657  cantnfp1  9664  carddomi2  9979  wdomfil  10068  fin1a2lem10  10415  fin1a2lem11  10416  uzsupss  12993  xaddcom  13296  xnegdi  13304  xpncan  13307  xleadd1a  13309  xsubge0  13317  ccat1st1st  14700  swrdccatin1  14798  sgncl  15174  cnpart  15331  fsumcllem  15822  fsumrev2  15872  expcnv  15957  geomulcvg  15969  fprodcllem  16044  fsumdvds  16404  gcd0id  16615  nn0seqcvgd  16666  lcmdvds  16704  mulgcddvds  16751  pcge0  16960  pcneg  16972  pcdvdstr  16974  pcz  16979  pcprmpw2  16980  pcadd  16987  ramcl2  17114  0ramcl  17121  ramub1lem1  17124  ramcl  17127  mrerintcl  17687  mreriincl  17688  mreexexlem4d  17741  mreclatBAD  18657  chnub  18716  psgnunilem1  19626  odmulg  19689  sylow1lem1  19731  pgpfi  19738  odadd1  19981  odadd2  19982  gsumval3  20040  gsumpt  20095  dprdfcntz  20150  dprd2da  20177  ablfac1eulem  20207  pgpfaclem3  20218  ablsimpgfind  20245  abvneg  20998  lssssr  21144  lspsneq  21315  lspdisj2  21320  drngnidl  21446  cnsubrg  21646  matunitlindf  22909  riinopn  23139  riincld  23275  neipeltop  23360  hauscmplem  23637  cmpfi  23639  ptbasfi  23813  xkoccn  23851  txindislem  23865  txtube  23872  hmphindis  24029  fclscmp  24262  utop2nei  24482  nrginvrcn  24924  nmoleub  24963  blcvx  25030  xrsxmet  25042  xrsblre  25044  lebnumlem3  25197  cphsqrtcl2  25420  ovollb2  25723  ioorcl  25811  i1fmulc  25937  itg1mulc  25938  mbfi1fseqlem4  25952  bddiblnc  26076  dvlip  26227  dvne0  26245  ig1pdvds  26412  plyeq0lem  26443  plyeq0  26444  aannenlem2  26572  aalioulem6  26580  abelthlem8  26682  abelth  26684  cxpexp  26913  cxpge0  26928  cxpmul2  26934  abscxp2  26938  abscxpbnd  26998  cxpeq  27002  nnlogbexp  27026  isosctrlem2  27064  atanrecl  27156  wilthlem2  27313  dchrabs2  27506  dchr1re  27507  lgsneg1  27566  lgsdirprm  27575  lgsdir  27576  lgsne0  27579  lgsdirnn0  27588  lgsdinn0  27589  2sqlem9  27671  rpvmasumlem  27731  dchrvmasumiflem1  27745  dchrisum0flblem1  27752  rpvmasum2  27756  pntrsumbnd2  27811  pntleml  27855  tgcgrextend  28834  tgbtwnexch2  28846  tgifscgr  28858  tgcolg  28904  tgidinside  28921  tgbtwnconn1lem2  28923  tgbtwnconn1lem3  28924  lnhl  28968  tglinethru  28991  tglineneq  29000  coltr  29003  coltr3  29004  colline  29005  tglnpt2  29008  tglnpt4  29010  mirreu3  29013  miriso  29029  mirln  29035  mirln2  29036  mirconn  29037  mirbtwnhl  29039  colmid  29047  krippenlem  29049  midexlem  29051  ragflat  29066  ragcgr  29069  perprag  29089  perpdragALT  29090  colperpexlem1  29093  colperpexlem3  29095  midex  29100  opphllem1  29110  opphllem2  29111  opphllem5  29114  opphllem6  29115  hlpasch  29121  lnincplng  29149  lnssplng  29157  mirplncl  29160  lmiisolem  29188  hypcgrlem1  29192  hypcgrlem2  29193  cgrg3col4  29259  prlnghpg  29311  perpprlng  29315  prlngmolem2  29318  prlngpln4  29323  prlngplngtr  29324  prlngmid2  29326  upgrex  29557  crctcshwlk  30298  crctcsh  30300  1wlkdlem2  30616  eupth2lem3lem3  30718  eupth2lem3lem7  30722  nmcoplbi  32517  nmophmi  32520  nmbdfnlbi  32538  disjdifprg  33056  imadifxp  33082  2ndimaxp  33127  mptiffisupp  33173  xlt2addrd  33238  ssnnssfz  33266  gsumpart  33511  suppgsumssiun  33520  symgcntz  33533  fzo0pmtrlast  33540  pmtridf1o  33542  pmtridfv1  33543  pmtridfv2  33544  psgnfzto1stlem  33548  tocycf  33565  cycpmco2lem5  33578  cycpmco2  33581  fxpgaval  33615  linds2eq  33822  dvdsruasso  33826  ply1coedeg  34007  ply1degltel  34012  ply1degleel  34013  ig1pmindeg  34020  esplyind  34093  fldext2chn  34246  constraddcl  34280  constrremulcl  34285  constrsqrtcl  34297  cos9thpiminplylem2  34301  locfinref  34359  zarcmplem  34399  esumpr2  34585  unelldsys  34677  sigapildsyslem  34680  sigapildsys  34681  mbfmcst  34778  carsgsigalem  34834  carsgclctunlem3  34839  pmeasmono  34843  probun  34938  0rrv  34970  signsvtn0  35086  signstfvneq0  35088  fineqvac  35650  wevgblacfn  35716  btwnconn1lem11  36685  finxp00  38164  poimirlem14  38391  mblfinlem1  38414  mblfinlem2  38415  ismblfin  38418  itg2addnclem  38428  itgaddnclem2  38436  areacirclem4  38468  areacirc  38470  isbnd3  38542  blbnd  38545  rrnequiv  38593  lsmsat  39889  lkrscss  39979  eqlkr  39980  lkrshpor  39988  atcvrj2b  40313  atltcvr  40316  3dim1  40348  3dim2  40349  3dim3  40350  ps-2  40359  2at0mat0  40406  dalemdnee  40547  dalem63  40616  lnatexN  40660  2llnma3r  40669  pmodlem1  40727  pmapjat1  40734  pclfinclN  40831  osumclN  40848  pexmidALTN  40859  lhpexle2lem  40890  lhpexle3lem  40892  4atexlemex6  40955  4atex  40957  trlnle  41067  trlval3  41068  cdlemc  41078  cdlemd9  41087  cdleme27N  41250  cdleme28c  41253  cdleme32fvaw  41320  cdleme42ke  41366  cdleme42keg  41367  cdleme42mgN  41369  cdleme17d  41379  cdleme48fvg  41381  cdleme50trn123  41435  cdlemb3  41487  cdlemg8  41512  cdlemg15a  41536  cdlemg15  41537  cdlemg16  41538  cdlemg16ALTN  41539  cdlemg16z  41540  cdlemg16zz  41541  cdlemg20  41566  cdlemg22  41568  cdlemg37  41570  cdlemg31d  41581  cdlemg39  41597  cdlemg40  41598  ltrncom  41619  tendotr  41711  cdlemk25-3  41785  cdlemk35s-id  41819  cdlemk39s-id  41821  cdlemk53b  41837  cdlemk53  41838  cdlemk55  41842  cdlemk35u  41845  cdlemk55u  41847  cdlemk39u  41849  cdlemk19u  41851  cdleml5N  41861  dia2dimlem7  41951  dia2dimlem13  41957  dih1dimatlem  42210  dihlsprn  42212  dihjat1lem  42309  dihjat1  42310  dvh2dim  42326  dochexmid  42349  lclkrlem1  42387  lclkrlem2i  42396  lclkrlem2t  42407  lcfrlem34  42457  lcfrlem38  42461  lcfrlem41  42464  mapdindp1  42601  mapdindp2  42602  mapdh6dN  42620  mapdh6jN  42626  mapdh8j  42668  mapdh8  42669  hdmap1l6d  42694  hdmap1l6j  42700  hdmap11lem2  42723  hdmap14lem7  42755  primrootlekpowne0  42979  aks6d1c7lem2  43055  unitscyglem4  43072  jm2.19  43842  jm2.23  43845  nzss  45149  disjxp1  45911  cnrefiisplem  46665  xlimliminflimsup  46698  stoweidlem58  46894  fourierdlem41  46984  fourierdlem48  46990  fouriersw  47067  etransclem24  47094  nnfoctbdjlem  47291  smfpimltxr  47583  smfpimgtxr  47616  chnerlem1  47718  sqrtqaa  47741  ssnn0ssfz  49287  mreclat  49931