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 2881  sdomdomtr 4449  mulgt0sr 5186  cnegextlem1 5317  muladdt 5393  divdiv23t 5748  divdivmult 5751  ltmul12it 5797  lemul12it 5800  lemulge11t 5804  lediv12it 5844  elfzle2 6416  elfz2nn0t 6427  fzrevt 6443  le2sqit 6563  bernneq 6583  fsumdivc 6973  fsumdivcALT 6974  fsum0diaglem2 7192  acdc2lem2 7431  acdc5lem2 7434  tgval3t 7567  tgss2t 7579  ssnei2 7671  cnpcl 7703  cnco 7707  cncnplem1 7713  cnconst 7719  blcntr 7785  blelrn 7788  blss 7793  opnuni 7808  metcnplem 7825  lmle 7895  xplmi 7907  lmcau 7930  cmsss 7931  bcthlem11 7943  grpidinvlem2 7983  grpinvid1 8006  grpinvid2 8007  grplcan 8010  abl4 8041  nvsubadd 8215  nvnpcan 8220  nvmeq0 8224  nvabs 8240  lnomul 8354  ubthlem3 8462  psasym 8576  5oalem5 9520  unoplint 9760  hmoplint 9782  bralnfnt 9788  hmopst 9860  hmopmt 9861  hmopcot 9863  adjaddt 9940  kbass3t 9963  strlem3a 10089  csmdsym 10169  ghomf1olem 10301  trnij 10481  imonclem 10583  idmon 10588

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