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

Theorem pm2.61ian 766
 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 424 . 2
3 pm2.61ian.2 . . 3
43ex 424 . 2
52, 4pm2.61i 158 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wa 359 This theorem is referenced by:  4cases  916  consensus  926  sbcom  2164  ax11indalem  2273  tfindsg  4832  findsg  4864  xpcan2  5298  ixpexg  7078  fipwss  7426  ranklim  7762  fin23lem14  8205  fzoval  11133  iswrdi  11723  ressbas  13511  resslem  13514  ressinbas  13517  cntzval  15112  sralem  16241  srasca  16245  sravsca  16246  ocvval  16886  tnglem  18673  tngds  18681  unopbd  23510  nmopcoi  23590  dsmmval  27168  afvres  28003  afvco2  28007  iswrd0i  28146  swrdccatin12  28180  swrdccat  28182  2cshw  28222  2cshwmod  28223  2cshwcom  28230  cshwssizelem2  28244  sbcomwAUX7  29525  sbcomOLD7  29692 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 178  df-an 361
 Copyright terms: Public domain W3C validator