MPE Home 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  |-  ( (
ph  /\  ps )  ->  ch )
pm2.61ian.2  |-  ( ( -.  ph  /\  ps )  ->  ch )
Assertion
Ref Expression
pm2.61ian  |-  ( ps 
->  ch )

Proof of Theorem pm2.61ian
StepHypRef Expression
1 pm2.61ian.1 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
21ex 424 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 pm2.61ian.2 . . 3  |-  ( ( -.  ph  /\  ps )  ->  ch )
43ex 424 . 2  |-  ( -. 
ph  ->  ( ps  ->  ch ) )
52, 4pm2.61i 158 1  |-  ( ps 
->  ch )
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