Theorem pm2.61dane 3031

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ≠ wne 2942

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 396  df-ne 2943

This theorem is referenced by:  pm2.61da2ne  3032  pm2.61da3ne  3033  pm2.61iine  3034  disjxiun  5067  onfr  6290  f1oprswap  6743  soex  7742  riiner  8537  difsnen  8794  mapdom2  8884  nnunifi  8995  fofinf1o  9024  brwdom2  9262  cantnff  9362  cantnfp1  9369  carddomi2  9659  wdomfil  9748  fin1a2lem10  10096  fin1a2lem11  10097  uzsupss  12609  xaddcom  12903  xnegdi  12911  xpncan  12914  xleadd1a  12916  xsubge0  12924  ccat1st1st  14263  swrdccatin1  14366  cnpart  14879  fsumcllem  15372  fsumrev2  15422  expcnv  15504  geomulcvg  15516  fprodcllem  15589  fsumdvds  15945  gcd0id  16154  nn0seqcvgd  16203  lcmdvds  16241  mulgcddvds  16288  pcge0  16491  pcneg  16503  pcdvdstr  16505  pcz  16510  pcprmpw2  16511  pcadd  16518  ramcl2  16645  0ramcl  16652  ramub1lem1  16655  ramcl  16658  mrerintcl  17223  mreriincl  17224  mreexexlem4d  17273  mreclatBAD  18196  psgnunilem1  19016  odmulg  19078  sylow1lem1  19118  pgpfi  19125  odadd1  19364  odadd2  19365  gsumval3  19423  gsumpt  19478  dprdfcntz  19533  dprd2da  19560  ablfac1eulem  19590  pgpfaclem3  19601  ablsimpgfind  19628  abvneg  20009  lssssr  20130  lspsneq  20299  lspdisj2  20304  drngnidl  20413  cnsubrg  20570  riinopn  21965  riincld  22103  neipeltop  22188  hauscmplem  22465  cmpfi  22467  ptbasfi  22640  xkoccn  22678  txindislem  22692  txtube  22699  hmphindis  22856  fclscmp  23089  utop2nei  23310  nrginvrcn  23762  nmoleub  23801  blcvx  23867  xrsxmet  23878  xrsblre  23880  lebnumlem3  24032  cphsqrtcl2  24255  ovollb2  24558  ioorcl  24646  i1fmulc  24773  itg1mulc  24774  mbfi1fseqlem4  24788  bddiblnc  24911  dvlip  25062  dvne0  25080  ig1pdvds  25246  plyeq0lem  25276  plyeq0  25277  aannenlem2  25394  aalioulem6  25402  abelthlem8  25503  abelth  25505  cxpexp  25728  cxpge0  25743  cxpmul2  25749  abscxp2  25753  abscxpbnd  25811  cxpeq  25815  nnlogbexp  25836  isosctrlem2  25874  atanrecl  25966  wilthlem2  26123  dchrabs2  26315  dchr1re  26316  lgsneg1  26375  lgsdirprm  26384  lgsdir  26385  lgsne0  26388  lgsdirnn0  26397  lgsdinn0  26398  2sqlem9  26480  rpvmasumlem  26540  dchrvmasumiflem1  26554  dchrisum0flblem1  26561  rpvmasum2  26565  pntrsumbnd2  26620  pntleml  26664  tgcgrextend  26750  tgbtwnexch2  26761  tgifscgr  26773  tgcolg  26819  tgidinside  26836  tgbtwnconn1lem2  26838  tgbtwnconn1lem3  26839  lnhl  26880  tglinethru  26901  tglnpt2  26906  tglineneq  26909  coltr  26912  coltr3  26913  colline  26914  mirreu3  26919  miriso  26935  mirln  26941  mirln2  26942  mirconn  26943  mirbtwnhl  26945  colmid  26953  krippenlem  26955  midexlem  26957  ragflat  26969  ragcgr  26972  perprag  26991  perpdragALT  26992  colperpexlem1  26995  colperpexlem3  26997  midex  27002  opphllem1  27012  opphllem2  27013  opphllem5  27016  opphllem6  27017  hlpasch  27021  lmiisolem  27061  hypcgrlem1  27064  hypcgrlem2  27065  cgrg3col4  27118  upgrex  27365  crctcshwlk  28088  crctcsh  28090  1wlkdlem2  28403  eupth2lem3lem3  28495  eupth2lem3lem7  28499  nmcoplbi  30291  nmophmi  30294  nmbdfnlbi  30312  disjdifprg  30815  imadifxp  30841  2ndimaxp  30885  xlt2addrd  30983  ssnnssfz  31010  gsumpart  31217  symgcntz  31256  pmtridf1o  31263  pmtridfv1  31264  pmtridfv2  31265  psgnfzto1stlem  31269  tocycf  31286  cycpmco2lem5  31299  cycpmco2  31302  linds2eq  31477  locfinref  31693  zarcmplem  31733  esumpr2  31935  unelldsys  32026  sigapildsyslem  32029  sigapildsys  32030  mbfmcst  32126  carsgsigalem  32182  carsgclctunlem3  32187  pmeasmono  32191  probun  32286  0rrv  32318  sgncl  32405  signsvtn0  32449  signstfvneq0  32451  fineqvac  32966  frxp2  33718  frxp3  33724  btwnconn1lem11  34326  finxp00  35500  matunitlindf  35702  poimirlem14  35718  mblfinlem1  35741  mblfinlem2  35742  ismblfin  35745  itg2addnclem  35755  itgaddnclem2  35763  areacirclem4  35795  areacirc  35797  isbnd3  35869  blbnd  35872  rrnequiv  35920  lsmsat  36949  lkrscss  37039  eqlkr  37040  lkrshpor  37048  atcvrj2b  37373  atltcvr  37376  3dim1  37408  3dim2  37409  3dim3  37410  ps-2  37419  2at0mat0  37466  dalemdnee  37607  dalem63  37676  lnatexN  37720  2llnma3r  37729  pmodlem1  37787  pmapjat1  37794  pclfinclN  37891  osumclN  37908  pexmidALTN  37919  lhpexle2lem  37950  lhpexle3lem  37952  4atexlemex6  38015  4atex  38017  trlnle  38127  trlval3  38128  cdlemc  38138  cdlemd9  38147  cdleme27N  38310  cdleme28c  38313  cdleme32fvaw  38380  cdleme42ke  38426  cdleme42keg  38427  cdleme42mgN  38429  cdleme17d  38439  cdleme48fvg  38441  cdleme50trn123  38495  cdlemb3  38547  cdlemg8  38572  cdlemg15a  38596  cdlemg15  38597  cdlemg16  38598  cdlemg16ALTN  38599  cdlemg16z  38600  cdlemg16zz  38601  cdlemg20  38626  cdlemg22  38628  cdlemg37  38630  cdlemg31d  38641  cdlemg39  38657  cdlemg40  38658  ltrncom  38679  tendotr  38771  cdlemk25-3  38845  cdlemk35s-id  38879  cdlemk39s-id  38881  cdlemk53b  38897  cdlemk53  38898  cdlemk55  38902  cdlemk35u  38905  cdlemk55u  38907  cdlemk39u  38909  cdlemk19u  38911  cdleml5N  38921  dia2dimlem7  39011  dia2dimlem13  39017  dih1dimatlem  39270  dihlsprn  39272  dihjat1lem  39369  dihjat1  39370  dvh2dim  39386  dochexmid  39409  lclkrlem1  39447  lclkrlem2i  39456  lclkrlem2t  39467  lcfrlem34  39517  lcfrlem38  39521  lcfrlem41  39524  mapdindp1  39661  mapdindp2  39662  mapdh6dN  39680  mapdh6jN  39686  mapdh8j  39728  mapdh8  39729  hdmap1l6d  39754  hdmap1l6j  39760  hdmap11lem2  39783  hdmap14lem7  39815  jm2.19  40731  jm2.23  40734  nzss  41824  disjxp1  42506  cnrefiisplem  43260  xlimliminflimsup  43293  stoweidlem58  43489  fourierdlem41  43579  fourierdlem48  43585  fouriersw  43662  etransclem24  43689  nnfoctbdjlem  43883  ssnn0ssfz  45573  mreclat  46171