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  2029  ax11indalem  2136  tfindsg  4651  findsg  4683  xpcan2  5113  ixpexg  6840  fipwss  7182  ranklim  7516  fin23lem14  7959  fzoval  10876  iswrdi  11417  ressbas  13198  resslem  13201  ressinbas  13204  cntzval  14797  sralem  15930  srasca  15934  sravsca  15935  ocvval  16567  tnglem  18156  tngds  18164  unopbd  22595  nmopcoi  22675  iintlem1  25610  pdiveql  26168  dsmmval  27200  afvres  28034  afvco2  28037
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