Theorem pm2.61ian 831

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

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

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 197  df-an 386

This theorem is referenced by:  4cases  990  cases2  993  consensus  999  sbcrextOLD  3512  csbexg  4792  xpcan2  5571  tfindsg  7060  findsg  7093  ixpexg  7932  fipwss  8335  ranklim  8707  fin23lem14  9155  fzoval  12471  modsumfzodifsn  12743  hashge2el2dif  13262  iswrdi  13309  ffz0iswrd  13332  swrd0  13434  swrdsbslen  13448  swrdspsleq  13449  swrdccatin12  13491  swrdccat  13493  repswswrd  13531  cshword  13537  cshwcsh2id  13574  dvdsabseq  15035  m1exp1  15093  flodddiv4  15137  dfgcd2  15263  lcmftp  15349  prmop1  15742  fvprmselelfz  15748  ressbas  15930  resslem  15933  ressinbas  15936  cntzval  17754  symg2bas  17818  sralem  19177  srasca  19181  sravsca  19182  sraip  19183  ocvval  20011  dsmmval  20078  dmatmul  20303  1mavmul  20354  mavmul0g  20359  1marepvmarrepid  20381  smadiadetglem2  20478  1elcpmat  20520  decpmatid  20575  tnglem  22444  tngds  22452  gausslemma2dlem1a  25090  2lgslem1c  25118  uvtxa01vtx  26298  clwlkclwwlklem2a4  26898  clwlkclwwlklem2a  26899  clwwisshclwwsn  26929  eucrctshift  27103  eucrct2eupth  27105  unopbd  28874  nmopcoi  28954  resvsca  29830  resvlem  29831  noprefixmo  31848  nosupno  31849  nosupbday  31851  nosupbnd1lem5  31858  nosupbnd1  31860  nosupbnd2  31862  ax12indalem  34230  afvres  41252  afvco2  41256  2ffzoeq  41338  pfxccatin12  41425  pfxccat3a  41429  cshword2  41437  ply1mulgsumlem2  42175  lcoel0  42217  lindslinindsimp1  42246  difmodm1lt  42317  digexp  42401  dig1  42402