Theorem simplr 449

Description: Simplification of a conjunction.

Assertion

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

Proof of Theorem simplr

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

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  simp1lr 940  simp2lr 944  simp3lr 948  ax11indalem 1759  ax11inda2ALT 1760  ordelord 3680  reuuniss2 3817  fvelimabOLD 4726  reiotass2 5111  odi 5258  omsmo 5314  ac6sfilem3 5508  riota5 5580  onomeneq 5612  ordiso 5683  hartoglem 5692  hartog 5693  noinfep 5747  elomsubsd 5885  infenomsub 5889  prpssnq 6246  cnegexlem2 6500  cnegexlem3 6501  divdivdiv 6961  divdivdivOLD 6962  ltmul12a 7023  lemulge11 7030  lt2mul2div 7054  lediv12a 7079  lediv2a 7080  nndiv 7143  zltp1le 7390  zdiv 7397  iccsupr 7567  elfzelz 7652  fzrev 7689  fzrev3 7692  fsequb2 7703  exprecOLD 7838  expmul 7840  expnbnd 7901  seq1bndi 8162  caubndi 8178  fsumsplit 8280  fsumcom 8288  fsumdivc 8295  clm4lei 8341  climcmpc1 8399  climsqueeze 8400  climsqueeze2 8401  cvgratlem5 8516  opnssneib 9005  clslp 9024  cnpco 9046  iscncl 9047  dnsconst 9065  blval 9114  blcntr 9122  blelrn 9125  ssblex 9133  lpbl 9157  metcnplem 9164  tgioolem 9192  lmconst 9212  lmnn 9213  iscau3 9216  iscau4 9218  xplm 9253  cmsss 9275  grpidinvlem4 9331  grprid 9346  ssga 9455  gapmlem 9461  vacnlem3 9669  nmcnilem 9676  sm1cnilem 9686  nvcnpi3 9761  nvcnpi4 9762  fipreima 10175  txcn 10227  subtopmet 10256  hausfillim 10303  cncomp 10331  tosdir 10358  hvmul0or 10526  hhsscms 10783  spansncol 11124  osumlem6 11218  3oalem2 11243  eigposi 11399  hhlnoi 11463  unoplin 11481  hmoplin 11503  hmopco 11585  lnopconi 11600  lnfnconi 11627  cnlnadjlem6 11642  kbass4 11690  nmopleid 11710  dmdbr2 11875  dmdbr5 11880  mdslmd1lem1 11897  mdslmd1lem2 11898  superpos 11926  irredlem1 11962  bnj1098 12917  axdense 14027  axfelem5 14035  axfelem16 14046  ranncnt 14625  dfdir2 14639  mgmlion 14697  resgcom 14712  curgrpact 14735  fprodsub 14742  trran2 14757  topindis 14859  qusp 14908  usptoplem 14917  istopx 14918  stfincomp 14959  iintlem1 15010  flimfneicn 15037  supnuf 15041  imonclem 15162  ismonc 15163  icmpmon 15165  iepiclem 15172  isepic 15173  elfiun 15369  fictb 15371  finsschain 15373  ordisoOLD 15374  hartoglemOLD 15383  hartogOLD 15384  elomsubsdOLD 15394  infenomsubOLD 15398  cnsubsp 15426  cnsubsp2 15427  alexsublem4 15440  alexsub 15441  cnconn 15444  reconnlem3 15448  reconnlem4 15449  reconnlem5 15450  2ndcsb 15476  isfne3 15482  topfneec 15501  fnessref 15503  neibastop2lem3 15521  neibastop2lem4 15522  neibastop2 15523  neibastop3 15524  topjoin 15527  fnemeet2 15529  filssufillem 15570  ufileu 15573  ufinffr 15578  ufilen 15579  limfilcf 15587  flimcls 15588  rnelfmlem 15592  fmfnfm 15598  flimfcnp 15602  isfclus 15606  fclsfnflim 15614  fcluscnp 15618  filnetlem4 15643  filnetlem5 15644  filnet 15645  fipreimaOLD 15756  frfi 15771  sdclem2 15810  sdc 15811  blssp 15844  mettrifi 15847  geomcau 15849  iocopnst 15877  hmeocld 15900  sstotbnd 15936  totbndbnd 15944  ismtyhmeolem 15950  heiborlem13 15967  heiborlem18 15972  heiborlem36 15990  rrndstprj1 16017  rrntotbndlem1 16020  rrntotbnd 16022  phtpyco 16056  reparpht 16065  pcohtpy 16083  crnghomfo 16154  lubid 16807  glbcon 17028  hlhght2 17038  hlatmstc 17047  atltcvr 17072  grpidinvlem4NEW 17112  grpridNEW 17121  pmapat 17243  paddasslem5 17285  pmapjoin 17313  pmapjat 17314  osumcl 17375  pexmid 17377  pexmidlem8 17385

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 164  df-an 242

Copyright terms: Public domain