Theorem pm2.61ian 798

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 436	. 2 |- ( ph -> ( ps -> ch ) )
3		pm2.61ian.2	. . 3 |- ( ( -. ph /\ ps ) -> ch )
4	3	ex 436	. 2 |- ( -. ph -> ( ps -> ch ) )
5	2, 4	pm2.61i 168	1 |- ( ps -> ch )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 371

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 189  df-an 373

This theorem is referenced by:  4cases  958  consensus  968  cases2  981  sbcrext  3374  csbexg  4556  xpcan2  5291  tfindsg  6699  findsg  6732  ixpexg  7552  fipwss  7947  ranklim  8318  fin23lem14  8765  fzoval  11923  hashge2el2dif  12635  iswrdi  12673  ffz0iswrd  12692  swrd0  12786  swrdsbslen  12800  swrdspsleq  12801  swrdccatin12  12843  swrdccat  12845  repswswrd  12883  cshword  12889  cshwcsh2id  12923  lcmftp  14602  prmop1  14989  fvprmselelfz  14995  ressbas  15172  resslem  15175  ressinbas  15178  cntzval  16968  symg2bas  17032  sralem  18393  srasca  18397  sravsca  18398  sraip  18399  ocvval  19222  dsmmval  19289  dmatmul  19514  1mavmul  19565  mavmul0g  19570  1marepvmarrepid  19592  smadiadetglem2  19689  1elcpmat  19731  decpmatid  19786  tnglem  21640  tngds  21648  clwlkisclwwlklem2a4  25504  clwlkisclwwlklem2a  25505  clwwisshclwwn  25528  unopbd  27660  nmopcoi  27740  resvsca  28595  resvlem  28596  ax12indalem  32441  afvres  38392  afvco2  38396  pfxccatin12  38684  pfxccat3a  38688  cshword2  38696  2ffzoeq  38759  ply1mulgsumlem2  39485  lcoel0  39527  lindslinindsimp1  39556  difmodm1lt  39631  digexp  39724  dig1  39725