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

Theorem pm2.61ian 790
Description: Elimination of an antecedent. (Contributed by NM, 1-Jan-2005.)
Hypotheses
Ref Expression
pm2.61ian.1
pm2.61ian.2
Assertion
Ref Expression
pm2.61ian

Proof of Theorem pm2.61ian
StepHypRef Expression
1 pm2.61ian.1 . . 3
21ex 434 . 2
3 pm2.61ian.2 . . 3
43ex 434 . 2
52, 4pm2.61i 164 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  /\wa 369
This theorem is referenced by:  4cases  949  consensus  959  cases2  971  ax12indalem  2275  sbcrext  3410  csbexg  4584  xpcan2  5449  tfindsg  6695  findsg  6727  ixpexg  7513  fipwss  7909  ranklim  8283  fin23lem14  8734  fzoval  11830  hashge2el2dif  12521  iswrdi  12552  ffz0iswrd  12568  swrd0  12658  swrdspsleq  12673  swrdccatin12  12716  swrdccat  12718  repswswrd  12756  cshword  12762  cshwcsh2id  12796  ressbas  14687  resslem  14690  ressinbas  14693  cntzval  16359  symg2bas  16423  sralem  17823  srasca  17827  sravsca  17828  sraip  17829  ocvval  18698  dsmmval  18765  dmatmul  18999  1mavmul  19050  mavmul0g  19055  1marepvmarrepid  19077  smadiadetglem2  19174  1elcpmat  19216  decpmatid  19271  tnglem  21154  tngds  21162  clwlkisclwwlklem2a4  24784  clwlkisclwwlklem2a  24785  clwwisshclwwn  24808  unopbd  26934  nmopcoi  27014  resvsca  27820  resvlem  27821  afvres  32257  afvco2  32261  2ffzoeq  32341  ply1mulgsumlem2  32987  lcoel0  33029  lindslinindsimp1  33058
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 185  df-an 371
  Copyright terms: Public domain W3C validator