Theorem simpll 412

Description: Simplification of a conjunction.

Assertion

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

Proof of Theorem simpll

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

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  sspr 2466  ordelord 2960  oaass 4179  ltexpq 5052  prn0 5065  cnegextlem1 5317  cnegext 5320  conjmult 5753  ltmul12it 5797  lemul12it 5800  zltp1let 6128  elfzel1 6413  elfz2nn0t 6427  fzrevt 6443  expaddt 6527  expmult 6528  expmwordit 6537  cvg2 6859  caubnd 6863  bcclt 6910  fsumsplit 6958  fsumcom 6966  fsumdivc 6973  fsumdivcALT 6974  climsub 7066  climsqueeze 7076  climsqueeze2 7077  climcau 7092  caucvg 7099  cvgcmp3c 7122  isum1p 7141  reccnv 7153  cvgratlem1 7185  efaddlem23 7302  acdc3lem 7428  acdc2lem1 7430  acdc2lem2 7431  acdc5lem2 7434  acdclem 7436  infdif 7511  tgss2t 7579  neissex 7679  clslp 7689  dnsconst 7727  ssblex 7796  opnuni 7808  lpbl 7819  metcnplem 7825  tgioolem 7853  lmbr 7866  lmle 7895  xplm 7909  lmcau 7930  cmsss 7931  bcthlem16 7948  bcthlem30 7962  grpidinvlem4 7985  grpideu 7987  grpidinv2 7994  grplid 7995  abl4 8041  blocnilem 8395  ubthlem5 8464  hvmul0ort 8815  shex 8998  3oalem2 9525  bralnfnt 9788  kbpjt 9796  eighmortht 9804  hmopmt 9861  hmopcot 9863  lnopcon 9878  lnfncon 9905  riesz3 9910  cnlnadjlem6 9920  adjmult 9939  kbass5t 9965  leopmulit 9978  nmopleidt 9983  dmdbr2 10140  mdslmd1lem1 10160  superpos 10189  irredlem2 10226  irred 10229  atcvat4 10232  cdrci 10381  qusp 10430  iintlem1 10476  icmpmon 10587  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