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

Theorem pm2.61ian 765
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 423 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 pm2.61ian.2 . . 3  |-  ( ( -.  ph  /\  ps )  ->  ch )
43ex 423 . 2  |-  ( -. 
ph  ->  ( ps  ->  ch ) )
52, 4pm2.61i 156 1  |-  ( ps 
->  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 358
This theorem is referenced by:  4cases  915  consensus  925  sbcom  2042  ax11indalem  2149  tfindsg  4667  findsg  4699  xpcan2  5129  ixpexg  6856  fipwss  7198  ranklim  7532  fin23lem14  7975  fzoval  10892  iswrdi  11433  ressbas  13214  resslem  13217  ressinbas  13220  cntzval  14813  sralem  15946  srasca  15950  sravsca  15951  ocvval  16583  tnglem  18172  tngds  18180  unopbd  22611  nmopcoi  22691  iintlem1  25713  pdiveql  26271  dsmmval  27303  afvres  28140  afvco2  28144  sbcomwAUX7  29562  sbcomOLD7  29709
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 177  df-an 360
  Copyright terms: Public domain W3C validator