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  947  consensus  957  cases2  970  ax12indalem  2268  sbcrext  3414  csbexg  4579  xpcan2  5443  tfindsg  6674  findsg  6706  ixpexg  7493  fipwss  7888  ranklim  8261  fin23lem14  8712  fzoval  11797  hashge2el2dif  12486  iswrdi  12517  ffz0iswrd  12533  swrd0  12620  swrdspsleq  12635  swrdccatin12  12678  swrdccat  12680  repswswrd  12718  cshword  12724  cshwcsh2id  12758  ressbas  14544  resslem  14547  ressinbas  14550  cntzval  16161  symg2bas  16225  sralem  17618  srasca  17622  sravsca  17623  sraip  17624  ocvval  18481  dsmmval  18548  dmatmul  18782  1mavmul  18833  mavmul0g  18838  1marepvmarrepid  18860  smadiadetglem2  18957  1elcpmat  18999  decpmatid  19054  tnglem  20905  tngds  20913  clwlkisclwwlklem2a4  24476  clwlkisclwwlklem2a  24477  clwwisshclwwn  24500  unopbd  26626  nmopcoi  26706  resvsca  27499  resvlem  27500  afvres  31740  afvco2  31744  2ffzoeq  31824  ply1mulgsumlem2  32077  lcoel0  32119  lindslinindsimp1  32148