Theorem pm2.61dane 3029

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ≠ wne 2940

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 207  df-an 396  df-ne 2941

This theorem is referenced by:  pm2.61da2ne  3030  pm2.61da3ne  3031  pm2.61iine  3032  disjxiun  5140  onfr  6423  f1oprswap  6892  soex  7943  frxp2  8169  frxp3  8176  riiner  8830  difsnen  9093  mapdom2  9188  nnunifi  9327  fofinf1o  9372  brwdom2  9613  cantnff  9714  cantnfp1  9721  carddomi2  10010  wdomfil  10101  fin1a2lem10  10449  fin1a2lem11  10450  uzsupss  12982  xaddcom  13282  xnegdi  13290  xpncan  13293  xleadd1a  13295  xsubge0  13303  ccat1st1st  14666  swrdccatin1  14763  cnpart  15279  fsumcllem  15768  fsumrev2  15818  expcnv  15900  geomulcvg  15912  fprodcllem  15987  fsumdvds  16345  gcd0id  16556  nn0seqcvgd  16607  lcmdvds  16645  mulgcddvds  16692  pcge0  16900  pcneg  16912  pcdvdstr  16914  pcz  16919  pcprmpw2  16920  pcadd  16927  ramcl2  17054  0ramcl  17061  ramub1lem1  17064  ramcl  17067  mrerintcl  17640  mreriincl  17641  mreexexlem4d  17690  mreclatBAD  18608  psgnunilem1  19511  odmulg  19574  sylow1lem1  19616  pgpfi  19623  odadd1  19866  odadd2  19867  gsumval3  19925  gsumpt  19980  dprdfcntz  20035  dprd2da  20062  ablfac1eulem  20092  pgpfaclem3  20103  ablsimpgfind  20130  abvneg  20827  lssssr  20952  lspsneq  21124  lspdisj2  21129  drngnidl  21253  cnsubrg  21445  riinopn  22914  riincld  23052  neipeltop  23137  hauscmplem  23414  cmpfi  23416  ptbasfi  23589  xkoccn  23627  txindislem  23641  txtube  23648  hmphindis  23805  fclscmp  24038  utop2nei  24259  nrginvrcn  24713  nmoleub  24752  blcvx  24819  xrsxmet  24831  xrsblre  24833  lebnumlem3  24995  cphsqrtcl2  25220  ovollb2  25524  ioorcl  25612  i1fmulc  25738  itg1mulc  25739  mbfi1fseqlem4  25753  bddiblnc  25877  dvlip  26032  dvne0  26050  ig1pdvds  26219  plyeq0lem  26249  plyeq0  26250  aannenlem2  26371  aalioulem6  26379  abelthlem8  26483  abelth  26485  cxpexp  26710  cxpge0  26725  cxpmul2  26731  abscxp2  26735  abscxpbnd  26796  cxpeq  26800  nnlogbexp  26824  isosctrlem2  26862  atanrecl  26954  wilthlem2  27112  dchrabs2  27306  dchr1re  27307  lgsneg1  27366  lgsdirprm  27375  lgsdir  27376  lgsne0  27379  lgsdirnn0  27388  lgsdinn0  27389  2sqlem9  27471  rpvmasumlem  27531  dchrvmasumiflem1  27545  dchrisum0flblem1  27552  rpvmasum2  27556  pntrsumbnd2  27611  pntleml  27655  tgcgrextend  28493  tgbtwnexch2  28504  tgifscgr  28516  tgcolg  28562  tgidinside  28579  tgbtwnconn1lem2  28581  tgbtwnconn1lem3  28582  lnhl  28623  tglinethru  28644  tglnpt2  28649  tglineneq  28652  coltr  28655  coltr3  28656  colline  28657  mirreu3  28662  miriso  28678  mirln  28684  mirln2  28685  mirconn  28686  mirbtwnhl  28688  colmid  28696  krippenlem  28698  midexlem  28700  ragflat  28712  ragcgr  28715  perprag  28734  perpdragALT  28735  colperpexlem1  28738  colperpexlem3  28740  midex  28745  opphllem1  28755  opphllem2  28756  opphllem5  28759  opphllem6  28760  hlpasch  28764  lmiisolem  28804  hypcgrlem1  28807  hypcgrlem2  28808  cgrg3col4  28861  upgrex  29109  crctcshwlk  29842  crctcsh  29844  1wlkdlem2  30157  eupth2lem3lem3  30249  eupth2lem3lem7  30253  nmcoplbi  32047  nmophmi  32050  nmbdfnlbi  32068  disjdifprg  32588  imadifxp  32614  2ndimaxp  32656  mptiffisupp  32702  xlt2addrd  32762  ssnnssfz  32789  chnub  33002  gsumpart  33060  symgcntz  33105  fzo0pmtrlast  33112  pmtridf1o  33114  pmtridfv1  33115  pmtridfv2  33116  psgnfzto1stlem  33120  tocycf  33137  cycpmco2lem5  33150  cycpmco2  33153  linds2eq  33409  dvdsruasso  33413  ply1degltel  33615  ply1degleel  33616  ig1pmindeg  33622  fldext2chn  33769  locfinref  33840  zarcmplem  33880  esumpr2  34068  unelldsys  34159  sigapildsyslem  34162  sigapildsys  34163  mbfmcst  34261  carsgsigalem  34317  carsgclctunlem3  34322  pmeasmono  34326  probun  34421  0rrv  34453  sgncl  34541  signsvtn0  34585  signstfvneq0  34587  fineqvac  35111  wevgblacfn  35114  btwnconn1lem11  36098  finxp00  37403  matunitlindf  37625  poimirlem14  37641  mblfinlem1  37664  mblfinlem2  37665  ismblfin  37668  itg2addnclem  37678  itgaddnclem2  37686  areacirclem4  37718  areacirc  37720  isbnd3  37791  blbnd  37794  rrnequiv  37842  lsmsat  39009  lkrscss  39099  eqlkr  39100  lkrshpor  39108  atcvrj2b  39434  atltcvr  39437  3dim1  39469  3dim2  39470  3dim3  39471  ps-2  39480  2at0mat0  39527  dalemdnee  39668  dalem63  39737  lnatexN  39781  2llnma3r  39790  pmodlem1  39848  pmapjat1  39855  pclfinclN  39952  osumclN  39969  pexmidALTN  39980  lhpexle2lem  40011  lhpexle3lem  40013  4atexlemex6  40076  4atex  40078  trlnle  40188  trlval3  40189  cdlemc  40199  cdlemd9  40208  cdleme27N  40371  cdleme28c  40374  cdleme32fvaw  40441  cdleme42ke  40487  cdleme42keg  40488  cdleme42mgN  40490  cdleme17d  40500  cdleme48fvg  40502  cdleme50trn123  40556  cdlemb3  40608  cdlemg8  40633  cdlemg15a  40657  cdlemg15  40658  cdlemg16  40659  cdlemg16ALTN  40660  cdlemg16z  40661  cdlemg16zz  40662  cdlemg20  40687  cdlemg22  40689  cdlemg37  40691  cdlemg31d  40702  cdlemg39  40718  cdlemg40  40719  ltrncom  40740  tendotr  40832  cdlemk25-3  40906  cdlemk35s-id  40940  cdlemk39s-id  40942  cdlemk53b  40958  cdlemk53  40959  cdlemk55  40963  cdlemk35u  40966  cdlemk55u  40968  cdlemk39u  40970  cdlemk19u  40972  cdleml5N  40982  dia2dimlem7  41072  dia2dimlem13  41078  dih1dimatlem  41331  dihlsprn  41333  dihjat1lem  41430  dihjat1  41431  dvh2dim  41447  dochexmid  41470  lclkrlem1  41508  lclkrlem2i  41517  lclkrlem2t  41528  lcfrlem34  41578  lcfrlem38  41582  lcfrlem41  41585  mapdindp1  41722  mapdindp2  41723  mapdh6dN  41741  mapdh6jN  41747  mapdh8j  41789  mapdh8  41790  hdmap1l6d  41815  hdmap1l6j  41821  hdmap11lem2  41844  hdmap14lem7  41876  primrootlekpowne0  42106  aks6d1c7lem2  42182  unitscyglem4  42199  jm2.19  43005  jm2.23  43008  nzss  44336  disjxp1  45074  cnrefiisplem  45844  xlimliminflimsup  45877  stoweidlem58  46073  fourierdlem41  46163  fourierdlem48  46169  fouriersw  46246  etransclem24  46273  nnfoctbdjlem  46470  smfpimltxr  46762  smfpimgtxr  46795  ssnn0ssfz  48265  mreclat  48886