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

Theorem idd 24
Description: Principle of identity with antecedent. (Contributed by NM, 26-Nov-1995.)
Assertion
Ref Expression
idd  |-  ( ph  ->  ( ps  ->  ps ) )

Proof of Theorem idd
StepHypRef Expression
1 id 22 . 2  |-  ( ps 
->  ps )
21a1i 11 1  |-  ( ph  ->  ( ps  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  imim1d  75  simprim  150  pm2.6  170  pm2.65  172  orel2  383  pm2.621  408  simpr  458  ancld  548  ancrd  549  anim12d  558  anim1d  559  anim2d  560  pm2.63  779  orim1d  828  orim2d  829  ecase2d  924  cad0  1445  merco2  1546  spnfw  1722  r19.36av  2858  r19.44av  2867  r19.45av  2868  eqsbc3r  3236  reuss  3619  opthpr  4038  wereu2  4704  relop  4977  soxp  6674  omopth2  7011  swoord2  7119  mapdom2  7470  en3lplem2  7809  rankxplim3  8076  cfsmolem  8427  fin1a2s  8571  fpwwe2lem12  8795  fpwwe2lem13  8796  inawina  8844  gchina  8853  elnnz  10643  xmullem  11214  ioopnfsup  11686  icopnfsup  11687  expeq0  11877  repswswrd  12405  repswcshw  12429  vdwlem6  14029  lublecllem  15140  tsrlemax  15372  ocv2ss  17939  0top  18429  neindisj2  18568  lmconst  18706  cnpresti  18733  sslm  18744  cmpfi  18852  bwthOLD  18855  dfcon2  18864  hausflim  19395  bndth  20371  nmoleub2a  20513  nmoleub2b  20514  cmetcaulem  20640  ioorf  20894  ioorinv2  20896  itg2mulclem  21065  itg2mulc  21066  dgrcolem2  21625  plydiveu  21648  psercnlem2  21773  dvloglem  21977  axcontlem4  23035  grponnncan2  23563  dipsubdir  24070  icossicc  25880  iocssicc  25881  ioossico  25882  idinside  27961  endofsegid  27962  meran1  28104  onsuct0  28134  ftc1anclem7  28314  nn0prpwlem  28358  nn0prpw  28359  fdc1  28483  rngosubdi  28600  rngosubdir  28601  mpt2bi123f  28816  mptbi12f  28820  stoweidlem27  29665  stoweidlem31  29669  stoweidlem35  29673  stoweidlem60  29698  atbiffatnnb  29770  usgfiregdegfi  30371  3ornot23  30911  rspsbc2  30938  sbcim2g  30943  idn2  31034  idn3  31036  trsspwALT2  31252  sspwtrALT  31255  sstrALT2  31270  bj-sngltag  32056  lkreqN  32385  cdlemg33a  33920  mapdordlem2  34852
  Copyright terms: Public domain W3C validator