Theorem simprl 450

Description: Simplification of a conjunction.

Assertion

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

Proof of Theorem simprl

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

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  simp1rl 941  simp2rl 945  simp3rl 949  xp0r 4065  imainss 4331  unielxp 5047  1stconst 5070  2ndconst 5071  ac6sfilem3 5508  ordiso 5683  ordtypelem6 5689  ordtypelem7 5690  hartog 5693  rankxplim3 5825  muladdOLD 6583  xrre 6744  divadddiv 6960  divdivdiv 6961  divdivdivOLD 6962  conjmul 6975  ltmul12a 7023  lemulge11 7030  ledivp1 7088  modmul1 7519  elfzle1 7653  2shfti 7765  expordi 7845  le2sq2 7877  expnbnd 7901  fsumcom 8288  fsummulc1 8293  fsumdivc 8295  serzcmp0 8315  climaddc1 8378  climaddc2 8379  climsubc2 8391  climcmpc1 8399  cvgratlem5 8516  cnpnei 9043  blelrn 9125  blss 9130  metequiv 9158  lmbr 9206  lmnn 9213  lmsslem 9230  metelcls 9243  metcnp4 9248  xplmi 9251  lmcau 9274  grpidinvlem1 9328  grpidinvlem2 9329  grpinvid1 9356  grpinvid2 9357  grplcan 9359  ssga 9455  nvmf 9598  nvsubadd 9607  nvnpcan 9612  nvabs 9633  nvlmle 9665  lnomul 9760  blocnilem 9804  ubthlem7 9878  ubthlem8 9879  ubthlem10 9881  minveclem30 9919  htthlem10 9976  psdmrn 9991  psref 9992  elsubsp 10248  subtopmetlem 10255  subtopmet 10256  fbssint 10279  fbunfip 10282  elfilmap3 10314  tosdir 10358  spansncol 11124  unoplin 11481  hmoplin 11503  hmops 11582  hmopm 11583  hmopco 11585  lnopconi 11600  lnfnconi 11627  adjmul 11662  adjadd 11663  mdslmd1lem1 11897  atn0 11917  irredi 11966  mdsymlem3 11977  bnj168 12496  ghomf1olem 13637  wfi 13915  frind 13939  axdenselem5 14023  axfelem5 14035  axfelem13 14043  axfelem15 14045  cljo 14534  clme 14535  jidd 14540  midd 14541  ubpar 14603  definc 14621  domncnt 14624  ranncnt 14625  toplat 14638  dfdir2 14639  resgcom 14712  fprodadd 14713  curgrpact 14735  fprodsub 14742  sub2vec 14815  mvecrtol 14816  iscnp3 14946  trnij 15015  dualcat2 15133  idmon 15166  taralt 15211  finsschain 15373  ordisoOLD 15374  ordtypelem6OLD 15380  ordtypelem7OLD 15381  hartogOLD 15384  subntr 15425  cnsubsp 15426  alexsublem3 15439  alexsublem4 15440  dfcon2 15442  reconnlem2 15447  reconnlem4 15449  reconnlem5 15450  2ndcsb 15476  2ndcctbss 15478  isfne3 15482  fnetr 15495  reftr 15497  fnessref 15503  refssfne 15504  locfincf 15516  comppfsc 15517  neibastop1 15518  neibastop2lem2 15520  neibastop3 15524  topjoin 15527  fnemeet1 15528  fnemeet2 15529  isufil2 15565  filssufil 15571  filufint 15574  fixufil 15576  ufinffr 15578  ufilen 15579  limfilcf 15587  cnpfillim 15589  rnelfmlem 15592  rnelfm 15593  fmfnfmlem2 15595  fmfnfmlem4 15597  fmufil 15599  isfclus 15606  fcluscf 15612  fclsfnflim 15614  flimfnfcls 15615  fcluscnp 15618  fcluscomplem 15620  filnetlem3 15642  filnetlem4 15643  filnetlem5 15644  sdc 15811  fdc 15812  fdc1 15813  subspopn 15837  subspcld 15838  blhalf 15846  lmtlm 15908  txsubsp 15912  ismtyhmeolem 15950  ismtybndlem 15952  heiborlem18 15972  heiborlem36 15990  rrncms 16019  rrntotbndlem2 16021  phtpyco 16056  pcohtpy 16083  pi1gp 16095  iscringd 16147  idlsubcl 16171  unichnidl 16179  hlsuprexch 17033  cvr1 17054  cvratlem 17061  grpidinvlem1NEW 17109  grpidinvlem2NEW 17110  grpinvid1NEW 17131  grpinvid2NEW 17132  grplcanNEW 17134  isline2 17248  paddcom 17274  paddss12 17280  paddasslem4 17284  paddasslem6 17286  paddasslem7 17287  paddasslem10 17290  pmodlem2 17308  pmodl42 17312  pmapjoin 17313  poml4 17361  osumcllem4 17367  pexmidlem1 17378  pexmidlem3 17380  pexmidlem4 17381  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