MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.61dane Unicode version

Theorem pm2.61dane 2524
Description: Deduction eliminating an inequality in an antecedent. (Contributed by NM, 30-Nov-2011.)
Hypotheses
Ref Expression
pm2.61dane.1  |-  ( (
ph  /\  A  =  B )  ->  ps )
pm2.61dane.2  |-  ( (
ph  /\  A  =/=  B )  ->  ps )
Assertion
Ref Expression
pm2.61dane  |-  ( ph  ->  ps )

Proof of Theorem pm2.61dane
StepHypRef Expression
1 pm2.61dane.1 . . 3  |-  ( (
ph  /\  A  =  B )  ->  ps )
21ex 423 . 2  |-  ( ph  ->  ( A  =  B  ->  ps ) )
3 pm2.61dane.2 . . 3  |-  ( (
ph  /\  A  =/=  B )  ->  ps )
43ex 423 . 2  |-  ( ph  ->  ( A  =/=  B  ->  ps ) )
52, 4pm2.61dne 2523 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1623    =/= wne 2446
This theorem is referenced by:  pm2.61da2ne  2525  pm2.61da3ne  2526  disjxiun  4020  onfr  4431  soex  5122  f1oprswap  5515  riiner  6732  difsnen  6944  mapdom2  7032  nnunifi  7108  fofinf1o  7137  brwdom2  7287  cantnff  7375  cantnfp1  7383  carddomi2  7603  wdomfil  7688  fin1a2lem10  8035  fin1a2lem11  8036  uzsupss  10310  xaddcom  10565  xnegdi  10568  xpncan  10571  xleadd1a  10573  xsubge0  10581  cnpart  11725  fsumcllem  12205  fsumrev2  12244  expcnv  12322  geomulcvg  12332  fsumdvds  12572  gcd0id  12702  nn0seqcvgd  12740  mulgcddvds  12783  pcge0  12914  pcneg  12926  pcdvdstr  12928  pcz  12933  pcprmpw2  12934  pcadd  12937  ramcl2  13063  0ramcl  13070  ramub1lem1  13073  ramcl  13076  mrerintcl  13499  mreriincl  13500  mreexexlem4d  13549  mreclat  14290  odmulg  14869  sylow1lem1  14909  pgpfi  14916  odadd1  15140  odadd2  15141  gsumval3  15191  gsumpt  15222  dprdfcntz  15250  dprd2da  15277  ablfac1eulem  15307  pgpfaclem3  15318  abvneg  15599  lssssr  15710  lspsneq  15875  lspdisj2  15880  drngnidl  15981  cnsubrg  16432  riinopn  16654  riincld  16781  hauscmplem  17133  cmpfi  17135  ptbasfi  17276  xkoccn  17313  txindislem  17327  txtube  17334  hmphindis  17488  fclscmp  17725  nrginvrcn  18202  nmoleub  18240  blcvx  18304  xrsxmet  18315  xrsblre  18317  lebnumlem3  18461  cphsqrcl2  18622  ovollb2  18848  ioorcl  18932  i1fmulc  19058  itg1mulc  19059  mbfi1fseqlem4  19073  dvlip  19340  dvne0  19358  ig1pdvds  19562  plyeq0lem  19592  plyeq0  19593  aannenlem2  19709  aalioulem6  19717  abelthlem8  19815  abelth  19817  cxpexp  20015  cxpge0  20030  cxpmul2  20036  abscxp2  20040  abscxpbnd  20093  cxpeq  20097  isosctrlem2  20119  atanrecl  20207  wilthlem2  20307  dchrabs2  20501  dchr1re  20502  lgsneg1  20559  lgsdirprm  20568  lgsdir  20569  lgsne0  20572  lgsdirnn0  20578  lgsdinn0  20579  2sqlem9  20612  rpvmasumlem  20636  dchrvmasumiflem1  20650  dchrisum0flblem1  20657  rpvmasum2  20661  pntrsumbnd2  20716  pntleml  20760  nmcoplbi  22608  nmophmi  22611  nmbdfnlbi  22629  xlt2addrd  23253  disjdifprg  23352  esumpr2  23439  mbfmcst  23564  probun  23622  0rrv  23654  umgraex  23875  eupath2lem3  23903  btwnconn1lem11  24720  areacirclem5  24929  areacirc  24931  efilcp  25552  isbnd3  26508  blbnd  26511  rrnequiv  26559  jm2.19  27086  jm2.23  27089  psgnunilem1  27416  lsmsat  29198  lkrscss  29288  eqlkr  29289  lkrshpor  29297  atcvrj2b  29621  atltcvr  29624  3dim1  29656  3dim2  29657  3dim3  29658  ps-2  29667  2at0mat0  29714  dalemdnee  29855  dalem63  29924  lnatexN  29968  2llnma3r  29977  pmodlem1  30035  pmapjat1  30042  pclfinclN  30139  osumclN  30156  pexmidALTN  30167  lhpexle2lem  30198  lhpexle3lem  30200  4atexlemex6  30263  4atex  30265  trlnle  30375  trlval3  30376  cdlemc  30386  cdlemd9  30395  cdleme27N  30558  cdleme28c  30561  cdleme32fvaw  30628  cdleme42ke  30674  cdleme42keg  30675  cdleme42mgN  30677  cdleme17d  30687  cdleme48fvg  30689  cdleme50trn123  30743  cdlemb3  30795  cdlemg8  30820  cdlemg15a  30844  cdlemg15  30845  cdlemg16  30846  cdlemg16ALTN  30847  cdlemg16z  30848  cdlemg16zz  30849  cdlemg20  30874  cdlemg22  30876  cdlemg37  30878  cdlemg31d  30889  cdlemg39  30905  cdlemg40  30906  ltrncom  30927  tendotr  31019  cdlemk25-3  31093  cdlemk35s-id  31127  cdlemk39s-id  31129  cdlemk53b  31145  cdlemk53  31146  cdlemk55  31150  cdlemk35u  31153  cdlemk55u  31155  cdlemk39u  31157  cdlemk19u  31159  cdleml5N  31169  dia2dimlem7  31260  dia2dimlem13  31266  dih1dimatlem  31519  dihlsprn  31521  dihjat1lem  31618  dihjat1  31619  dvh2dim  31635  dochexmid  31658  lclkrlem1  31696  lclkrlem2i  31705  lclkrlem2t  31716  lcfrlem34  31766  lcfrlem38  31770  lcfrlem41  31773  mapdindp1  31910  mapdindp2  31911  mapdh6dN  31929  mapdh6jN  31935  mapdh8j  31978  mapdh8  31979  hdmap1l6d  32004  hdmap1l6j  32010  hdmap11lem2  32035  hdmap14lem7  32067
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-ne 2448
  Copyright terms: Public domain W3C validator