Theorem pm2.61ian 804

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

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

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 190  df-an 377

This theorem is referenced by:  4cases  966  consensus  976  cases2  989  sbcrext  3352  csbexg  4550  xpcan2  5292  tfindsg  6713  findsg  6746  ixpexg  7571  fipwss  7968  ranklim  8340  fin23lem14  8788  fzoval  11951  hashge2el2dif  12669  iswrdi  12707  ffz0iswrd  12729  swrd0  12826  swrdsbslen  12840  swrdspsleq  12841  swrdccatin12  12883  swrdccat  12885  repswswrd  12923  cshword  12929  cshwcsh2id  12963  lcmftp  14657  prmop1  15044  fvprmselelfz  15050  ressbas  15227  resslem  15230  ressinbas  15233  cntzval  17023  symg2bas  17087  sralem  18448  srasca  18452  sravsca  18453  sraip  18454  ocvval  19278  dsmmval  19345  dmatmul  19570  1mavmul  19621  mavmul0g  19626  1marepvmarrepid  19648  smadiadetglem2  19745  1elcpmat  19787  decpmatid  19842  tnglem  21696  tngds  21704  clwlkisclwwlklem2a4  25560  clwlkisclwwlklem2a  25561  clwwisshclwwn  25584  unopbd  27716  nmopcoi  27796  resvsca  28641  resvlem  28642  ax12indalem  32560  afvres  38711  afvco2  38715  pfxccatin12  39005  pfxccat3a  39009  cshword2  39017  2ffzoeq  39105  uvtxa01vtx  39519  ply1mulgsumlem2  40451  lcoel0  40493  lindslinindsimp1  40522  difmodm1lt  40597  digexp  40690  dig1  40691