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

Theorem pm2.61ian 788
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 432 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 pm2.61ian.2 . . 3  |-  ( ( -.  ph  /\  ps )  ->  ch )
43ex 432 . 2  |-  ( -. 
ph  ->  ( ps  ->  ch ) )
52, 4pm2.61i 164 1  |-  ( ps 
->  ch )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 367
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 369
This theorem is referenced by:  4cases  947  consensus  957  cases2  969  ax12indalem  2277  sbcrext  3398  csbexg  4571  xpcan2  5429  tfindsg  6668  findsg  6700  ixpexg  7486  fipwss  7881  ranklim  8253  fin23lem14  8704  fzoval  11805  hashge2el2dif  12505  iswrdi  12537  ffz0iswrd  12556  swrd0  12650  swrdsbslen  12664  swrdspsleq  12665  swrdccatin12  12707  swrdccat  12709  repswswrd  12747  cshword  12753  cshwcsh2id  12787  ressbas  14773  resslem  14776  ressinbas  14779  cntzval  16558  symg2bas  16622  sralem  18018  srasca  18022  sravsca  18023  sraip  18024  ocvval  18871  dsmmval  18938  dmatmul  19166  1mavmul  19217  mavmul0g  19222  1marepvmarrepid  19244  smadiadetglem2  19341  1elcpmat  19383  decpmatid  19438  tnglem  21320  tngds  21328  clwlkisclwwlklem2a4  24986  clwlkisclwwlklem2a  24987  clwwisshclwwn  25010  unopbd  27132  nmopcoi  27212  resvsca  28055  resvlem  28056  afvres  32496  afvco2  32500  pfxccatin12  32653  pfxccat3a  32657  cshword2  32665  2ffzoeq  32715  ply1mulgsumlem2  33241  lcoel0  33283  lindslinindsimp1  33312  difmodm1lt  33389  digexp  33482  dig1  33483
  Copyright terms: Public domain W3C validator