Theorem simprl 414

Description: Simplification of a conjunction.

Assertion

Ref	Expression
simprl	|- ((ph /\ (ps /\ ch)) -> ps)

Proof of Theorem simprl

Step	Hyp	Ref	Expression
1		id 59	. 2 |- (ps -> ps)
2	1	ad2antrl 406	1 |- ((ph /\ (ps /\ ch)) -> ps)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  xp0r 3234  imainss 3455  unielxp 4097  rankxplim3 4694  cnegextlem1 5325  muladdt 5401  xrret 5550  divdiv23t 5756  conjmult 5761  ltmul12it 5805  lemulge11t 5812  ledivp1t 5861  2shft 6297  elfzle1 6423  expordit 6539  le2sqit 6571  expnbndt 6593  fsumcom 6974  fsummulc1 6979  fsumdivc 6981  serzcmp0 7001  climaddc1 7062  climaddc2 7063  climsubc2 7075  climcmpc1 7083  cvgratlem2 7194  cvgratlem5 7197  acdc3lem 7436  acdclem 7444  cnco 7718  blelrn 7800  blss 7805  metcnplem 7838  metcnpi3 7844  metcnpi4 7845  lmbr 7880  lmnn 7887  lmsslem 7903  metelcls 7916  metcnp4 7920  xplmi 7923  lmcau 7946  bcthlem21 7969  grpidinvlem1 7998  grpidinvlem2 7999  grpinvid1 8022  grpinvid2 8023  grplcan 8025  abl4 8056  nvmf 8218  nvsubadd 8227  nvnpcan 8232  nvabs 8253  nvlmle 8281  lnomul 8367  blocnilem 8408  blocni 8409  ubthlem3 8475  ubthlem7 8479  ubthlem8 8480  ubthlem10 8482  minveclem30 8518  htthlem10 8572  psdmrn 8591  psref 8592  spansncol 9430  unoplint 9783  hmoplint 9805  hmopst 9883  hmopmt 9884  hmopcot 9886  lnopcon 9901  lnfncon 9928  adjmult 9963  adjaddt 9964  mdslmd1lem1 10189  atn0 10209  irred 10258  mdsymlem3 10269  ghomf1olem 10330  gelsupvalOLD 10354  trnij 10517  imonclem 10619  idmon 10624

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain