Theorem pm2.61dane 3061

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

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1637   ≠ wne 2974

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 198  df-an 385  df-ne 2975

This theorem is referenced by:  pm2.61da2ne  3062  pm2.61da3ne  3063  pm2.61iine  3064  disjxiun  4834  onfr  5970  f1oprswap  6390  soex  7333  riiner  8049  difsnen  8275  mapdom2  8364  nnunifi  8444  fofinf1o  8474  brwdom2  8711  cantnff  8812  cantnfp1  8819  carddomi2  9073  wdomfil  9161  fin1a2lem10  9510  fin1a2lem11  9511  uzsupss  11993  xaddcom  12283  xnegdi  12290  xpncan  12293  xleadd1a  12295  xsubge0  12303  cnpart  14197  fsumcllem  14680  fsumrev2  14730  expcnv  14812  geomulcvg  14823  fprodcllem  14896  fsumdvds  15247  gcd0id  15453  nn0seqcvgd  15496  lcmdvds  15534  mulgcddvds  15581  pcge0  15777  pcneg  15789  pcdvdstr  15791  pcz  15796  pcprmpw2  15797  pcadd  15804  ramcl2  15931  0ramcl  15938  ramub1lem1  15941  ramcl  15944  mrerintcl  16456  mreriincl  16457  mreexexlem4d  16506  mreclatBAD  17386  psgnunilem1  18108  odmulg  18168  sylow1lem1  18208  pgpfi  18215  odadd1  18446  odadd2  18447  gsumval3  18503  gsumpt  18556  dprdfcntz  18610  dprd2da  18637  ablfac1eulem  18667  pgpfaclem3  18678  abvneg  19032  lssssr  19153  lssssrOLD  19154  lspsneq  19323  lspdisj2  19328  drngnidl  19432  cnsubrg  20008  riinopn  20920  riincld  21056  neipeltop  21141  hauscmplem  21417  cmpfi  21419  ptbasfi  21592  xkoccn  21630  txindislem  21644  txtube  21651  hmphindis  21808  fclscmp  22041  utop2nei  22261  nrginvrcn  22703  nmoleub  22742  blcvx  22808  xrsxmet  22819  xrsblre  22821  lebnumlem3  22969  cphsqrtcl2  23192  ovollb2  23464  ioorcl  23552  i1fmulc  23678  itg1mulc  23679  mbfi1fseqlem4  23693  dvlip  23964  dvne0  23982  ig1pdvds  24144  plyeq0lem  24174  plyeq0  24175  aannenlem2  24292  aalioulem6  24300  abelthlem8  24401  abelth  24403  cxpexp  24622  cxpge0  24637  cxpmul2  24643  abscxp2  24647  abscxpbnd  24702  cxpeq  24706  nnlogbexp  24727  isosctrlem2  24757  atanrecl  24846  wilthlem2  25003  dchrabs2  25195  dchr1re  25196  lgsneg1  25255  lgsdirprm  25264  lgsdir  25265  lgsne0  25268  lgsdirnn0  25277  lgsdinn0  25278  2sqlem9  25360  rpvmasumlem  25384  dchrvmasumiflem1  25398  dchrisum0flblem1  25405  rpvmasum2  25409  pntrsumbnd2  25464  pntleml  25508  tgcgrextend  25588  tgbtwnexch2  25599  tgifscgr  25611  tgcolg  25657  tgidinside  25674  tgbtwnconn1lem2  25676  tgbtwnconn1lem3  25677  lnhl  25718  tglinethru  25739  tglnpt2  25744  tglineneq  25747  coltr  25750  coltr3  25751  colline  25752  mirreu3  25757  miriso  25773  mirln  25779  mirln2  25780  mirconn  25781  mirbtwnhl  25783  colmid  25791  krippenlem  25793  midexlem  25795  ragflat  25807  ragcgr  25810  perprag  25826  perpdragALT  25827  colperpexlem1  25830  colperpexlem3  25832  midex  25837  opphllem1  25847  opphllem2  25848  opphllem5  25851  opphllem6  25852  hlpasch  25856  lmiisolem  25896  hypcgrlem1  25899  hypcgrlem2  25900  cgrg3col4  25942  upgrex  26195  crctcshwlk  26937  crctcsh  26939  1wlkdlem2  27305  eupth2lem3lem3  27397  eupth2lem3lem7  27401  nmcoplbi  29209  nmophmi  29212  nmbdfnlbi  29230  disjdifprg  29707  imadifxp  29733  xlt2addrd  29844  ssnnssfz  29870  psgnfzto1stlem  30169  pmtridf1o  30175  pmtridfv1  30176  pmtridfv2  30177  locfinref  30227  esumpr2  30448  unelldsys  30540  sigapildsyslem  30543  sigapildsys  30544  mbfmcst  30640  carsgsigalem  30696  carsgclctunlem3  30701  pmeasmono  30705  probun  30800  0rrv  30832  sgncl  30919  signsvtn0  30966  signstfvneq0  30968  btwnconn1lem11  32519  finxp00  33549  matunitlindf  33714  poimirlem14  33730  mblfinlem1  33753  mblfinlem2  33754  ismblfin  33757  itg2addnclem  33767  itgaddnclem2  33775  bddiblnc  33786  areacirclem4  33809  areacirc  33811  isbnd3  33888  blbnd  33891  rrnequiv  33939  lsmsat  34782  lkrscss  34872  eqlkr  34873  lkrshpor  34881  atcvrj2b  35206  atltcvr  35209  3dim1  35241  3dim2  35242  3dim3  35243  ps-2  35252  2at0mat0  35299  dalemdnee  35440  dalem63  35509  lnatexN  35553  2llnma3r  35562  pmodlem1  35620  pmapjat1  35627  pclfinclN  35724  osumclN  35741  pexmidALTN  35752  lhpexle2lem  35783  lhpexle3lem  35785  4atexlemex6  35848  4atex  35850  trlnle  35961  trlval3  35962  cdlemc  35972  cdlemd9  35981  cdleme27N  36144  cdleme28c  36147  cdleme32fvaw  36214  cdleme42ke  36260  cdleme42keg  36261  cdleme42mgN  36263  cdleme17d  36273  cdleme48fvg  36275  cdleme50trn123  36329  cdlemb3  36381  cdlemg8  36406  cdlemg15a  36430  cdlemg15  36431  cdlemg16  36432  cdlemg16ALTN  36433  cdlemg16z  36434  cdlemg16zz  36435  cdlemg20  36460  cdlemg22  36462  cdlemg37  36464  cdlemg31d  36475  cdlemg39  36491  cdlemg40  36492  ltrncom  36513  tendotr  36605  cdlemk25-3  36679  cdlemk35s-id  36713  cdlemk39s-id  36715  cdlemk53b  36731  cdlemk53  36732  cdlemk55  36736  cdlemk35u  36739  cdlemk55u  36741  cdlemk39u  36743  cdlemk19u  36745  cdleml5N  36755  dia2dimlem7  36845  dia2dimlem13  36851  dih1dimatlem  37104  dihlsprn  37106  dihjat1lem  37203  dihjat1  37204  dvh2dim  37220  dochexmid  37243  lclkrlem1  37281  lclkrlem2i  37290  lclkrlem2t  37301  lcfrlem34  37351  lcfrlem38  37355  lcfrlem41  37358  mapdindp1  37495  mapdindp2  37496  mapdh6dN  37514  mapdh6jN  37520  mapdh8j  37562  mapdh8  37563  hdmap1l6d  37588  hdmap1l6j  37594  hdmap11lem2  37617  hdmap14lem7  37649  jm2.19  38055  jm2.23  38058  nzss  39010  cnrefiisplem  40529  stoweidlem58  40748  fourierdlem41  40838  fourierdlem48  40844  fouriersw  40921  etransclem24  40948  nnfoctbdjlem  41145  ssnn0ssfz  42689