Theorem simplr 413

Description: Simplification of a conjunction.

Assertion

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

Proof of Theorem simplr

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

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  ax11indalem 1361  ax11inda2ALT 1362  reuuniss2 2881  ordelord 2960  fvelimab 3750  odi 4194  omsmo 4241  onomeneq 4498  noinfep 4612  prpssnq 5066  cnegextlem2 5318  cnegextlem3 5319  divmuldivt 5736  divdivmult 5751  ltmul12it 5797  lemulge11t 5804  lediv12it 5844  lediv2it 5845  nndivt 5906  zltp1let 6128  iccsupr 6331  elfzelz 6414  fzrevt 6443  fzrev3t 6446  fsequb2 6456  expmult 6528  expnbndt 6585  seq1bnd 6847  caubnd 6863  fsumsplit 6958  fsumcom 6966  fsumdivc 6973  clm4le 7019  climcmpc1 7075  climsqueeze 7076  climsqueeze2 7077  cvgratlem2 7186  cvgratlem5 7189  opnssneib 7670  clslp 7689  cnpco 7708  iscncl 7709  dnsconst 7727  blval 7777  blcntr 7785  blelrn 7788  ssblex 7796  lpbl 7819  metcnplem 7825  metcnp 7826  tgioolem 7853  lmconst 7872  lmnn 7873  iscau3 7876  xplm 7909  cmsss 7931  bcthlem2 7934  grpidinvlem4 7985  grprid 7996  abl4 8041  nmcnilem 8272  sm1cnilem 8281  nvcnpi4 8355  ubthlem5 8464  hvmul0ort 8815  hhsscms 9067  spansncol 9407  osumlem6 9500  3oalem2 9525  eigpos 9679  hhlno 9743  unoplint 9760  hmoplint 9782  hmopcot 9863  lnopcon 9878  lnfncon 9905  cnlnadjlem6 9920  kbass4t 9964  nmopleidt 9983  dmdbr2 10140  mdslmd1lem1 10160  mdslmd1lem2 10161  superpos 10189  irredlem1 10225  qusp 10430  iintlem1 10476  imonclem 10583  ismonc 10584  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