Theorem simprr 415

Description: Simplification of a conjunction.

Assertion

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

Proof of Theorem simprr

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

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  reuuniss2 2891  sdomdomtr 4469  mulgt0sr 5214  cnegextlem1 5345  muladdt 5421  divdiv23t 5792  divdivmult 5795  ltmul12it 5841  lemul12it 5844  lemulge11t 5848  lediv12it 5896  elfzle2 6484  elfz2nn0t 6495  fzrevt 6511  le2sqit 6632  bernneq 6652  fsumdivc 7035  fsumdivcALT 7036  fsum0diaglem2 7257  acdc2lem2 7489  acdc5lem2 7492  tgval3t 7625  tgss2t 7637  ssnei2 7730  cnpcl 7764  cnco 7768  cncnplem1 7774  cnconst 7780  blcntr 7845  blelrn 7848  blss 7853  opnuni 7868  metcnplem 7886  lmle 7960  xplmi 7973  lmcau 7996  cmsss 7997  bcthlem11 8009  grpidinvlem2 8049  grpinvid1 8072  grpinvid2 8073  grplcan 8075  abl4 8105  nvsubadd 8275  nvnpcan 8280  nvmeq0 8284  nvabs 8301  lnomul 8421  ubthlem3 8531  psasym 8651  spwpr3OLD 8662  5oalem5 9603  unoplint 9844  hmoplint 9866  bralnfnt 9872  hmopst 9945  hmopmt 9946  hmopcot 9948  adjaddt 10026  kbass3t 10051  strlem3a 10179  csmdsym 10261  ghomf1olem 10396  hmeobc 10542  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