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 1368  ax11inda2ALT 1369  reuuniss2 2891  ordelord 2970  fvelimab 3765  odi 4210  omsmo 4257  onomeneq 4519  noinfep 4640  prpssnq 5094  cnegextlem2 5346  cnegextlem3 5347  divmuldivt 5780  divdivmult 5795  ltmul12it 5841  lemulge11t 5848  lediv12it 5896  lediv2it 5897  nndivt 5959  zltp1let 6181  iccsupr 6398  elfzelz 6482  fzrevt 6511  fzrev3t 6514  fsequb2 6524  expmult 6597  expnbndt 6654  seq1bnd 6910  caubnd 6926  fsumsplit 7020  fsumcom 7028  fsumdivc 7035  clm4le 7081  climcmpc1 7139  climsqueeze 7140  climsqueeze2 7141  cvgratlem2 7251  cvgratlem5 7254  opnssneib 7729  clslp 7748  cnpco 7769  iscncl 7770  dnsconst 7788  blval 7837  blcntr 7845  blelrn 7848  ssblex 7856  lpbl 7880  metcnplem 7886  metcnp 7887  tgioolem 7914  lmconst 7934  lmnn 7935  iscau3 7938  iscau4 7940  xplm 7975  cmsss 7997  bcthlem2 8000  grpidinvlem4 8051  grprid 8062  abl4 8105  nmcnilem 8337  sm1cnilem 8347  nvcnpi3 8422  nvcnpi4 8423  ubthlem5 8533  spwpr4OLD 8663  spwpr4aOLD 8664  hvmul0ort 8894  hhsscms 9150  spansncol 9491  osumlem6 9583  3oalem2 9608  eigpos 9762  hhlno 9826  unoplint 9844  hmoplint 9866  hmopcot 9948  lnopcon 9963  lnfncon 9990  cnlnadjlem6 10005  kbass4t 10052  nmopleidt 10072  dmdbr2 10230  dmdbr5 10235  mdslmd1lem1 10252  mdslmd1lem2 10253  superpos 10281  irredlem1 10317  qusp 10555  iintlem1 10632  imonclem 10741  ismonc 10742  icmpmon 10744  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