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

Theorem eqnetrd 2464
Description: Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
Hypotheses
Ref Expression
eqnetrd.1  |-  ( ph  ->  A  =  B )
eqnetrd.2  |-  ( ph  ->  B  =/=  C )
Assertion
Ref Expression
eqnetrd  |-  ( ph  ->  A  =/=  C )

Proof of Theorem eqnetrd
StepHypRef Expression
1 eqnetrd.2 . 2  |-  ( ph  ->  B  =/=  C )
2 eqnetrd.1 . . 3  |-  ( ph  ->  A  =  B )
32neeq1d 2459 . 2  |-  ( ph  ->  ( A  =/=  C  <->  B  =/=  C ) )
41, 3mpbird 223 1  |-  ( ph  ->  A  =/=  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    =/= wne 2446
This theorem is referenced by:  eqnetrrd  2466  opnz  4242  frsn  4760  onoviun  6360  intrnfi  7170  cantnfp1lem2  7381  cantnfp1lem3  7382  wemapwe  7400  acndom2  7681  fin23lem14  7959  fin23lem40  7977  isf32lem6  7984  isf34lem5  8004  isf34lem7  8005  isf34lem6  8006  axcc2lem  8062  xaddnemnf  10561  xaddnepnf  10562  fseqsupcl  11039  hashprg  11368  limsupgre  11955  isercolllem3  12140  tanval3  12414  tanneg  12428  ruclem11  12518  phibndlem  12838  dfphi2  12842  0ram  13067  0ram2  13068  ram0  13069  0ramcl  13070  gsumval2  14460  issubg2  14636  ghmrn  14696  gsumval3  15191  pgpfaclem2  15317  ablfaclem2  15321  ablfaclem3  15322  abvdom  15603  lbsextlem2  15912  gzrngunit  16437  zrngunit  16438  iinopn  16648  cnconn  17148  1stcfb  17171  fbasrn  17579  fclscmpi  17724  alexsublem  17738  dscmet  18095  reperflem  18323  evth  18457  cmetcaulem  18714  iscmet3  18719  cmetss  18740  bcthlem5  18750  bcth2  18752  mbflimsup  19021  itg1addlem4  19054  itg1climres  19069  itg2monolem1  19105  itg2i1fseq2  19111  tdeglem4  19446  deg1add  19489  deg1mul2  19500  deg1tm  19504  dgreq  19626  dgradd2  19649  dgrmul  19651  dgrmulc  19652  dgrcolem1  19654  plyrem  19685  facth  19686  fta1lem  19687  vieta1lem1  19690  vieta1lem2  19691  vieta1  19692  qaa  19703  aareccl  19706  geolim3  19719  aaliou3lem9  19730  coseq00topi  19870  cosne0  19892  tanord  19900  tanarg  19970  cxpne0  20024  cxpsqr  20050  chordthmlem  20129  chordthmlem2  20130  dcubic  20142  mcubic  20143  cubic2  20144  cubic  20145  quartlem4  20156  atandmneg  20202  atandmcj  20205  atancj  20206  atanrecl  20207  atanlogsublem  20211  efiatan2  20213  tanatan  20215  atandmtan  20216  cosatan  20217  cosatanne0  20218  wilthlem2  20307  ftalem7  20316  basellem2  20319  basellem4  20321  basellem5  20322  isppw  20352  dchrptlem2  20504  lgsne0  20572  2sqlem8a  20610  2sqlem8  20611  cntnevol  23175  xaddeq0  23304  xrge0iifhom  23319  logccne0ALT  23398  logbrec  23407  derangenlem  23702  subfacp1lem3  23713  subfacp1lem5  23715  nobndlem8  24353  ivthALT  26258  neibastop1  26308  cmpfiiin  26772  pell1234qrne0  26938  rmxyneg  27005  bezoutr1  27073  fnwe2lem2  27148  kelac1  27161  frlmssuvc2  27247  pmtrmvd  27398  cnmsgnsubg  27434  stoweidlem23  27772  stoweidlem31  27780  wallispilem4  27817  wallispi  27819  stirlinglem3  27825  stirlinglem14  27836  elprchashprn2  28088  lsatfixedN  29199  islshpat  29207  lkrshp  29295  2llnm3N  29758  dalemdnee  29855  cdleme18b  30481  cdleme40m  30656  cdlemg12g  30838  cdlemh  31006  cdlemj3  31012  tendoconid  31018  cdlemk3  31022  cdlemk12  31039  cdlemk12u  31061  cdlemk46  31137  cdlemk54  31147  erngdvlem4  31180  erngdvlem4-rN  31188  dibn0  31343  dihglblem2aN  31483  dochshpncl  31574  dochsnnz  31640  dochsatshpb  31642  lcfl7lem  31689  lcfl8b  31694  lcfrlem33  31765  lcfr  31775  hdmaprnlem3uN  32044
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276  df-ne 2448
  Copyright terms: Public domain W3C validator