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 3239  imainss 3463  unielxp 4107  rankxplim3 4714  cnegextlem1 5345  muladdt 5421  xrret 5569  divdiv23t 5792  conjmult 5797  ltmul12it 5841  lemulge11t 5848  ledivp1t 5905  2shft 6352  elfzle1 6483  expordit 6600  le2sqit 6632  expnbndt 6654  fsumcom 7028  fsummulc1 7033  fsumdivc 7035  serzcmp0 7055  climaddc1 7118  climaddc2 7119  climsubc2 7131  climcmpc1 7139  cvgratlem2 7251  cvgratlem5 7254  acdc3lem 7486  acdclem 7494  cnco 7768  blelrn 7848  blss 7853  metcnplem 7886  metcnpi3 7892  metcnpi4 7893  lmbr 7928  lmnn 7935  lmsslem 7952  metelcls 7965  metcnp4 7970  xplmi 7973  lmcau 7996  bcthlem21 8019  grpidinvlem1 8048  grpidinvlem2 8049  grpinvid1 8072  grpinvid2 8073  grplcan 8075  abl4 8105  nvmf 8266  nvsubadd 8275  nvnpcan 8280  nvabs 8301  nvlmle 8333  lnomul 8421  blocnilem 8464  blocni 8465  ubthlem3 8531  ubthlem7 8535  ubthlem8 8536  ubthlem10 8538  minveclem30 8574  htthlem10 8629  psdmrn 8648  psref 8649  spansncol 9491  unoplint 9844  hmoplint 9866  hmopst 9945  hmopmt 9946  hmopcot 9948  lnopcon 9963  lnfncon 9990  adjmult 10025  adjaddt 10026  mdslmd1lem1 10252  atn0 10272  irred 10321  mdsymlem3 10332  ghomf1olem 10396  trnij 10637  imonclem 10741  idmon 10745

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