MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.61ian 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  2123  ax11indalem  2232  tfindsg  4781  findsg  4813  xpcan2  5247  ixpexg  7023  fipwss  7370  ranklim  7704  fin23lem14  8147  fzoval  11072  iswrdi  11659  ressbas  13447  resslem  13450  ressinbas  13453  cntzval  15048  sralem  16177  srasca  16181  sravsca  16182  ocvval  16818  tnglem  18553  tngds  18561  unopbd  23367  nmopcoi  23447  dsmmval  26870  afvres  27706  afvco2  27710  sbcomwAUX7  28924  sbcomOLD7  29072
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