Theorem pm2.61dane 3043

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559   ≠ wne 2956

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 209  df-an 400  df-ne 2957

This theorem is referenced by:  pm2.61da2ne  3044  pm2.61da3ne  3045  pm2.61iine  3046  disjxiun  5096  onfr  6381  f1oprswap  6848  soex  7898  frxp2  8119  frxp3  8126  riiner  8767  difsnen  9027  mapdom2  9116  nnunifi  9231  fofinf1o  9272  brwdom2  9518  cantnff  9626  cantnfp1  9633  carddomi2  9925  wdomfil  10014  fin1a2lem10  10363  fin1a2lem11  10364  uzsupss  12938  xaddcom  13240  xnegdi  13248  xpncan  13251  xleadd1a  13253  xsubge0  13261  ccat1st1st  14639  swrdccatin1  14735  cnpart  15250  fsumcllem  15742  fsumrev2  15792  expcnv  15877  geomulcvg  15889  fprodcllem  15964  fsumdvds  16325  gcd0id  16536  nn0seqcvgd  16587  lcmdvds  16625  mulgcddvds  16672  pcge0  16881  pcneg  16893  pcdvdstr  16895  pcz  16900  pcprmpw2  16901  pcadd  16908  ramcl2  17035  0ramcl  17042  ramub1lem1  17045  ramcl  17048  mrerintcl  17608  mreriincl  17609  mreexexlem4d  17662  mreclatBAD  18578  chnub  18637  psgnunilem1  19516  odmulg  19579  sylow1lem1  19621  pgpfi  19628  odadd1  19871  odadd2  19872  gsumval3  19930  gsumpt  19985  dprdfcntz  20040  dprd2da  20067  ablfac1eulem  20097  pgpfaclem3  20108  ablsimpgfind  20135  abvneg  20855  lssssr  21001  lspsneq  21172  lspdisj2  21177  drngnidl  21293  cnsubrg  21459  riinopn  22948  riincld  23084  neipeltop  23169  hauscmplem  23446  cmpfi  23448  ptbasfi  23621  xkoccn  23659  txindislem  23673  txtube  23680  hmphindis  23837  fclscmp  24070  utop2nei  24290  nrginvrcn  24732  nmoleub  24771  blcvx  24838  xrsxmet  24850  xrsblre  24852  lebnumlem3  25005  cphsqrtcl2  25228  ovollb2  25531  ioorcl  25619  i1fmulc  25745  itg1mulc  25746  mbfi1fseqlem4  25760  bddiblnc  25884  dvlip  26035  dvne0  26053  ig1pdvds  26220  plyeq0lem  26250  plyeq0  26251  aannenlem2  26370  aalioulem6  26378  abelthlem8  26479  abelth  26481  cxpexp  26710  cxpge0  26725  cxpmul2  26731  abscxp2  26735  abscxpbnd  26795  cxpeq  26799  nnlogbexp  26823  isosctrlem2  26861  atanrecl  26953  wilthlem2  27110  dchrabs2  27303  dchr1re  27304  lgsneg1  27363  lgsdirprm  27372  lgsdir  27373  lgsne0  27376  lgsdirnn0  27385  lgsdinn0  27386  2sqlem9  27468  rpvmasumlem  27528  dchrvmasumiflem1  27542  dchrisum0flblem1  27549  rpvmasum2  27553  pntrsumbnd2  27608  pntleml  27652  tgcgrextend  28631  tgbtwnexch2  28642  tgifscgr  28654  tgcolg  28700  tgidinside  28717  tgbtwnconn1lem2  28719  tgbtwnconn1lem3  28720  lnhl  28761  tglinethru  28782  tglnpt2  28787  tglineneq  28790  coltr  28793  coltr3  28794  colline  28795  mirreu3  28800  miriso  28816  mirln  28822  mirln2  28823  mirconn  28824  mirbtwnhl  28826  colmid  28834  krippenlem  28836  midexlem  28838  ragflat  28850  ragcgr  28853  perprag  28872  perpdragALT  28873  colperpexlem1  28876  colperpexlem3  28878  midex  28883  opphllem1  28893  opphllem2  28894  opphllem5  28897  opphllem6  28898  hlpasch  28902  lmiisolem  28942  hypcgrlem1  28945  hypcgrlem2  28946  cgrg3col4  28999  upgrex  29239  crctcshwlk  29968  crctcsh  29970  1wlkdlem2  30286  eupth2lem3lem3  30378  eupth2lem3lem7  30382  nmcoplbi  32177  nmophmi  32180  nmbdfnlbi  32198  disjdifprg  32724  imadifxp  32750  2ndimaxp  32798  mptiffisupp  32845  xlt2addrd  32911  ssnnssfz  32939  sgncl  32983  gsumpart  33204  suppgsumssiun  33213  symgcntz  33226  fzo0pmtrlast  33233  pmtridf1o  33235  pmtridfv1  33236  pmtridfv2  33237  psgnfzto1stlem  33241  tocycf  33258  cycpmco2lem5  33271  cycpmco2  33274  fxpgaval  33308  linds2eq  33528  dvdsruasso  33532  ply1coedeg  33746  ply1degltel  33751  ply1degleel  33752  ig1pmindeg  33759  esplyind  33833  fldext2chn  33986  constraddcl  34020  constrremulcl  34025  constrsqrtcl  34037  cos9thpiminplylem2  34041  locfinref  34099  zarcmplem  34139  esumpr2  34325  unelldsys  34416  sigapildsyslem  34419  sigapildsys  34420  mbfmcst  34517  carsgsigalem  34573  carsgclctunlem3  34578  pmeasmono  34582  probun  34677  0rrv  34709  signsvtn0  34828  signstfvneq0  34830  fineqvac  35376  wevgblacfn  35418  btwnconn1lem11  36411  finxp00  37860  matunitlindf  38081  poimirlem14  38097  mblfinlem1  38120  mblfinlem2  38121  ismblfin  38124  itg2addnclem  38134  itgaddnclem2  38142  areacirclem4  38174  areacirc  38176  isbnd3  38247  blbnd  38250  rrnequiv  38298  lsmsat  39596  lkrscss  39686  eqlkr  39687  lkrshpor  39695  atcvrj2b  40020  atltcvr  40023  3dim1  40055  3dim2  40056  3dim3  40057  ps-2  40066  2at0mat0  40113  dalemdnee  40254  dalem63  40323  lnatexN  40367  2llnma3r  40376  pmodlem1  40434  pmapjat1  40441  pclfinclN  40538  osumclN  40555  pexmidALTN  40566  lhpexle2lem  40597  lhpexle3lem  40599  4atexlemex6  40662  4atex  40664  trlnle  40774  trlval3  40775  cdlemc  40785  cdlemd9  40794  cdleme27N  40957  cdleme28c  40960  cdleme32fvaw  41027  cdleme42ke  41073  cdleme42keg  41074  cdleme42mgN  41076  cdleme17d  41086  cdleme48fvg  41088  cdleme50trn123  41142  cdlemb3  41194  cdlemg8  41219  cdlemg15a  41243  cdlemg15  41244  cdlemg16  41245  cdlemg16ALTN  41246  cdlemg16z  41247  cdlemg16zz  41248  cdlemg20  41273  cdlemg22  41275  cdlemg37  41277  cdlemg31d  41288  cdlemg39  41304  cdlemg40  41305  ltrncom  41326  tendotr  41418  cdlemk25-3  41492  cdlemk35s-id  41526  cdlemk39s-id  41528  cdlemk53b  41544  cdlemk53  41545  cdlemk55  41549  cdlemk35u  41552  cdlemk55u  41554  cdlemk39u  41556  cdlemk19u  41558  cdleml5N  41568  dia2dimlem7  41658  dia2dimlem13  41664  dih1dimatlem  41917  dihlsprn  41919  dihjat1lem  42016  dihjat1  42017  dvh2dim  42033  dochexmid  42056  lclkrlem1  42094  lclkrlem2i  42103  lclkrlem2t  42114  lcfrlem34  42164  lcfrlem38  42168  lcfrlem41  42171  mapdindp1  42308  mapdindp2  42309  mapdh6dN  42327  mapdh6jN  42333  mapdh8j  42375  mapdh8  42376  hdmap1l6d  42401  hdmap1l6j  42407  hdmap11lem2  42430  hdmap14lem7  42462  primrootlekpowne0  42686  aks6d1c7lem2  42762  unitscyglem4  42779  jm2.19  43534  jm2.23  43537  nzss  44857  disjxp1  45613  cnrefiisplem  46367  xlimliminflimsup  46400  stoweidlem58  46596  fourierdlem41  46686  fourierdlem48  46692  fouriersw  46769  etransclem24  46796  nnfoctbdjlem  46993  smfpimltxr  47285  smfpimgtxr  47318  chnerlem1  47422  ssnn0ssfz  48935  mreclat  49582