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

Step	Hyp	Ref	Expression
1		pm2.61ian.1	. . 3 |- ( ( ph /\ ps ) -> ch )
2	1	ex 432	. 2 |- ( ph -> ( ps -> ch ) )
3		pm2.61ian.2	. . 3 |- ( ( -. ph /\ ps ) -> ch )
4	3	ex 432	. 2 |- ( -. ph -> ( ps -> ch ) )
5	2, 4	pm2.61i 164	1 |- ( ps -> ch )

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