Theorem pm2.61dane 3042

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

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

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 2956

This theorem is used by:  pm2.61da2ne  3043  pm2.61da3ne  3044  pm2.61iine  3045  disjxiun  5099  onfr  6402  f1oprswap  6871  soex  7934  frxp2  8164  frxp3  8171  riiner  8815  difsnen  9082  mapdom2  9171  nnunifi  9287  fofinf1o  9325  brwdom2  9571  cantnff  9679  cantnfp1  9686  carddomi2  10055  wdomfil  10144  fin1a2lem10  10491  fin1a2lem11  10492  uzsupss  13071  xaddcom  13374  xnegdi  13382  xpncan  13385  xleadd1a  13387  xsubge0  13395  ccat1st1st  14781  swrdccatin1  14879  sgncl  15256  cnpart  15413  fsumcllem  15904  fsumrev2  15954  expcnv  16039  geomulcvg  16051  fprodcllem  16124  fsumdvds  16484  gcd0id  16697  nn0seqcvgd  16751  lcmdvds  16789  mulgcddvds  16836  pcge0  17046  pcneg  17058  pcdvdstr  17060  pcz  17065  pcprmpw2  17066  pcadd  17073  ramcl2  17200  0ramcl  17207  ramub1lem1  17210  ramcl  17213  mrerintcl  17773  mreriincl  17774  mreexexlem4d  17827  mreclatBAD  18743  chnub  18802  psgnunilem1  19713  odmulg  19776  sylow1lem1  19818  pgpfi  19825  odadd1  20068  odadd2  20069  gsumval3  20127  gsumpt  20182  dprdfcntz  20237  dprd2da  20264  ablfac1eulem  20294  pgpfaclem3  20305  ablsimpgfind  20332  abvneg  21089  lssssr  21235  lspsneq  21406  lspdisj2  21411  drngnidl  21537  cnsubrg  21739  matunitlindf  23002  riinopn  23232  riincld  23368  neipeltop  23453  hauscmplem  23730  cmpfi  23732  ptbasfi  23906  xkoccn  23944  txindislem  23958  txtube  23965  hmphindis  24122  fclscmp  24355  utop2nei  24575  nrginvrcn  25017  nmoleub  25056  blcvx  25123  xrsxmet  25135  xrsblre  25137  lebnumlem3  25290  cphsqrtcl2  25513  ovollb2  25816  ioorcl  25904  i1fmulc  26030  itg1mulc  26031  mbfi1fseqlem4  26045  bddiblnc  26168  dvlip  26319  dvne0  26337  ig1pdvds  26504  plyeq0lem  26535  plyeq0  26536  aannenlem2  26662  aalioulem6  26670  abelthlem8  26772  abelth  26774  cxpexp  27002  cxpge0  27017  cxpmul2  27023  abscxp2  27027  abscxpbnd  27087  cxpeq  27091  nnlogbexp  27115  isosctrlem2  27153  atanrecl  27245  wilthlem2  27402  dchrabs2  27595  dchr1re  27596  lgsneg1  27655  lgsdirprm  27664  lgsdir  27665  lgsne0  27668  lgsdirnn0  27677  lgsdinn0  27678  2sqlem9  27760  rpvmasumlem  27820  dchrvmasumiflem1  27834  dchrisum0flblem1  27841  rpvmasum2  27845  pntrsumbnd2  27900  pntleml  27944  tgcgrextend  28953  tgbtwnexch2  28965  tgifscgr  28977  tgcolg  29023  tgidinside  29040  tgbtwnconn1lem2  29042  tgbtwnconn1lem3  29043  lnhl  29087  tglinethru  29110  tglineneq  29119  coltr  29122  coltr3  29123  colline  29124  tglnpt2  29127  tglnpt4  29129  mirreu3  29132  miriso  29148  mirln  29154  mirln2  29155  mirconn  29156  mirbtwnhl  29158  colmid  29166  krippenlem  29168  midexlem  29170  ragflat  29185  ragcgr  29188  perprag  29208  perpdragALT  29209  colperpexlem1  29212  colperpexlem3  29214  midex  29219  opphllem1  29229  opphllem2  29230  opphllem5  29233  opphllem6  29234  hlpasch  29240  lnincplng  29268  lnssplng  29276  mirplncl  29279  lmiisolem  29307  hypcgrlem1  29311  hypcgrlem2  29312  cgrg3col4  29378  prlnghpg  29430  perpprlng  29434  prlngmolem2  29437  prlngpln4  29442  prlngplngtr  29443  prlngmid2  29445  upgrex  29676  crctcshwlk  30417  crctcsh  30419  1wlkdlem2  30735  eupth2lem3lem3  30837  eupth2lem3lem7  30841  nmcoplbi  32636  nmophmi  32639  nmbdfnlbi  32657  cgrgptxfr  33059  tgaas1h  33090  disjdifprg  33217  imadifxp  33243  2ndimaxp  33288  mptiffisupp  33334  xlt2addrd  33398  ssnnssfz  33426  gsumpart  33671  suppgsumssiun  33680  symgcntz  33693  fzo0pmtrlast  33700  pmtridf1o  33702  pmtridfv1  33703  pmtridfv2  33704  psgnfzto1stlem  33708  tocycf  33725  cycpmco2lem5  33738  cycpmco2  33741  fxpgaval  33775  linds2eq  33983  dvdsruasso  33987  ply1coedeg  34168  ply1degltel  34173  ply1degleel  34174  ig1pmindeg  34181  esplyind  34254  fldext2chn  34407  constraddcl  34441  constrremulcl  34446  constrsqrtcl  34458  cos9thpiminplylem2  34462  locfinref  34520  zarcmplem  34560  esumpr2  34746  unelldsys  34838  sigapildsyslem  34841  sigapildsys  34842  mbfmcst  34938  carsgsigalem  34994  carsgclctunlem3  34999  pmeasmono  35003  probun  35098  0rrv  35130  signsvtn0  35246  signstfvneq0  35248  fineqvac  35841  wevgblacfn  35959  btwnconn1lem11  36955  finxp00  38419  poimirlem14  38646  mblfinlem1  38669  mblfinlem2  38670  ismblfin  38673  itg2addnclem  38683  itgaddnclem2  38691  areacirclem4  38723  areacirc  38725  isbnd3  38812  blbnd  38815  rrnequiv  38863  lsmsat  40159  lkrscss  40249  eqlkr  40250  lkrshpor  40258  atcvrj2b  40583  atltcvr  40586  3dim1  40618  3dim2  40619  3dim3  40620  ps-2  40629  2at0mat0  40676  dalemdnee  40817  dalem63  40886  lnatexN  40930  2llnma3r  40939  pmodlem1  40997  pmapjat1  41004  pclfinclN  41101  osumclN  41118  pexmidALTN  41129  lhpexle2lem  41160  lhpexle3lem  41162  4atexlemex6  41225  4atex  41227  trlnle  41337  trlval3  41338  cdlemc  41348  cdlemd9  41357  cdleme27N  41520  cdleme28c  41523  cdleme32fvaw  41590  cdleme42ke  41636  cdleme42keg  41637  cdleme42mgN  41639  cdleme17d  41649  cdleme48fvg  41651  cdleme50trn123  41705  cdlemb3  41757  cdlemg8  41782  cdlemg15a  41806  cdlemg15  41807  cdlemg16  41808  cdlemg16ALTN  41809  cdlemg16z  41810  cdlemg16zz  41811  cdlemg20  41836  cdlemg22  41838  cdlemg37  41840  cdlemg31d  41851  cdlemg39  41867  cdlemg40  41868  ltrncom  41889  tendotr  41981  cdlemk25-3  42055  cdlemk35s-id  42089  cdlemk39s-id  42091  cdlemk53b  42107  cdlemk53  42108  cdlemk55  42112  cdlemk35u  42115  cdlemk55u  42117  cdlemk39u  42119  cdlemk19u  42121  cdleml5N  42131  dia2dimlem7  42221  dia2dimlem13  42227  dih1dimatlem  42480  dihlsprn  42482  dihjat1lem  42579  dihjat1  42580  dvh2dim  42596  dochexmid  42619  lclkrlem1  42657  lclkrlem2i  42666  lclkrlem2t  42677  lcfrlem34  42727  lcfrlem38  42731  lcfrlem41  42734  mapdindp1  42871  mapdindp2  42872  mapdh6dN  42890  mapdh6jN  42896  mapdh8j  42938  mapdh8  42939  hdmap1l6d  42964  hdmap1l6j  42970  hdmap11lem2  42993  hdmap14lem7  43025  primrootlekpowne0  43249  aks6d1c7lem2  43325  unitscyglem4  43342  jm2.19  44094  jm2.23  44097  nzss  45395  disjxp1  46180  cnrefiisplem  46933  xlimliminflimsup  46966  stoweidlem58  47162  fourierdlem41  47252  fourierdlem48  47258  fouriersw  47335  etransclem24  47362  nnfoctbdjlem  47559  smfpimltxr  47851  smfpimgtxr  47884  chnerlem1  47986  sqrtqaa  48009  ssnn0ssfz  49555  mreclat  50205