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

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

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 371

This theorem is referenced by:  4cases  940  consensus  950  ax12indalem  2246  sbcrext  3269  csbexg  4424  xpcan2  5275  tfindsg  6471  findsg  6503  ixpexg  7287  fipwss  7679  ranklim  8051  fin23lem14  8502  fzoval  11554  hashge2el2dif  12184  iswrdi  12239  ffz0iswrd  12255  swrd0  12327  swrdspsleq  12342  swrdccatin12  12382  swrdccat  12384  repswswrd  12422  cshword  12428  ressbas  14228  resslem  14231  ressinbas  14234  cntzval  15839  symg2bas  15903  sralem  17258  srasca  17262  sravsca  17263  sraip  17264  ocvval  18092  dsmmval  18159  1mavmul  18359  mavmul0g  18364  1marepvmarrepid  18386  smadiadetglem2  18478  tnglem  20226  tngds  20234  unopbd  25419  nmopcoi  25499  resvsca  26298  resvlem  26299  afvres  30078  afvco2  30082  2ffzoeq  30214  clwlkisclwwlklem2a4  30446  clwlkisclwwlklem2a  30447  clwwisshclwwn  30472  erclwwlktr0  30479  ply1mulgsumlem2  30845  dmatmul  30876  scmatsubcl  30884  scmatmulcl  30886  pmatcollpw1id  30899  lcoel0  30962  lindslinindsimp1  30991