Theorem simplrl 535

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

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

Proof of Theorem simplrl

Step	Hyp	Ref	Expression
1		simpl 109	. 2 |- ( ( ps /\ ch ) -> ps )
2	1	ad2antlr 489	1 |- ( ( ( ph /\ ( ps /\ ch ) ) /\ th ) -> ps )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  rmob  3056  disjiun  3999  f1imass  5775  riota5f  5855  tfrexlem  6335  tfrcl  6365  nnsucuniel  6496  nntr2  6504  fopwdom  6836  fidceq  6869  fisbth  6883  fientri3  6914  unsnfidcex  6919  undifdc  6923  iunfidisj  6945  fiuni  6977  ordiso2  7034  acfun  7206  2omotaplemap  7256  ccfunen  7263  addcmpblnq  7366  mulcmpblnq  7367  ordpipqqs  7373  addcmpblnq0  7442  mulcmpblnq0  7443  prml  7476  addlocpr  7535  prmuloc  7565  mullocpr  7570  ltexprlemopl  7600  ltexprlemopu  7602  ltexprlemloc  7606  ltexprlemrl  7609  ltexprlemru  7611  addcanprleml  7613  addcanprlemu  7614  aptiprleml  7638  ltmprr  7641  cauappcvgprlemopl  7645  cauappcvgprlemopu  7647  cauappcvgprlemloc  7651  caucvgprlemopl  7668  caucvgprlemopu  7670  caucvgprlemloc  7674  caucvgprprlemopu  7698  caucvgprprlemloc  7702  caucvgprprlemexbt  7705  caucvgprprlemaddq  7707  suplocexprlemrl  7716  suplocexprlemdisj  7719  suplocexprlemloc  7720  suplocexprlemub  7722  addcmpblnr  7738  mulcmpblnrlemg  7739  mulcmpblnr  7740  ltsrprg  7746  mulgt0sr  7777  caucvgsrlemgt1  7794  suplocsrlemb  7805  axmulcl  7865  axcaucvglemres  7898  axpre-suploclemres  7900  axpre-suploc  7901  cnegexlem1  8132  negeu  8148  add20  8431  apreap  8544  cru  8559  apsym  8563  apcotr  8564  apadd1  8565  apneg  8568  mulext1  8569  mulge0  8576  mulap0  8611  divdivdivap  8670  prodgt0  8809  ltmul12a  8817  lt2mul2div  8836  ledivdiv  8847  lediv12a  8851  qapne  9639  xleadd1a  9873  ixxss12  9906  elfz0ubfz0  10125  qtri3or  10243  exbtwnzlemstep  10248  exbtwnzlemex  10250  exbtwnz  10251  rebtwn2zlemstep  10253  rebtwn2z  10255  btwnzge0  10300  iseqf1olemqf1o  10493  mulexpzap  10560  leexp1a  10575  hashen  10764  fihashdom  10783  hashun  10785  cjap  10915  cvg1nlemres  10994  rsqrmo  11036  abslt  11097  abs3lem  11120  cau3lem  11123  rexanre  11229  xrmaxltsup  11266  climcau  11355  sumeq2  11367  summodc  11391  fisumss  11400  fsum2d  11443  fsumabs  11473  fsumiun  11485  prodeq2  11565  prodmodclem2  11585  fprodcl2lem  11613  fprodap0  11629  fprod2d  11631  fprodrec  11637  fprodap0f  11644  fprodle  11648  eirrap  11785  divalglemeunn  11926  divalglemeuneg  11928  bezoutlemnewy  11997  bezoutlemstep  11998  bezoutlemmain  11999  bezoutlembi  12006  bezoutlemeu  12008  qredeu  12097  isprm5lem  12141  pw2dvdseu  12168  sqrt2irrap  12180  pythagtriplem2  12266  pythagtrip  12283  pclemub  12287  pcqmul  12303  pcexp  12309  pcneg  12324  pcprmpw2  12332  pcadd  12339  prmpwdvds  12353  ennnfonelemg  12404  ennnfonelemrnh  12417  ctiunctlemfo  12440  nninfdclemf1  12453  imasival  12727  ismndd  12838  mndpropd  12841  mhmeql  12876  mhmmnd  12980  mulgfng  12987  issubg4m  13053  ssnmz  13071  ringpropd  13217  dvdsrtr  13270  islmod  13381  restbasg  13671  cnpnei  13722  cnptoprest2  13743  cnpdis  13745  lmtopcnp  13753  txcnp  13774  ismet2  13857  blininf  13927  metss2lem  14000  xmettxlem  14012  xmettx  14013  metcnp  14015  metcnpi3  14020  addcncntoplem  14054  fsumcncntop  14059  mulc1cncf  14079  cncfco  14081  mulcncf  14094  dedekindeulemuub  14098  dedekindeu  14104  dedekindicclemuub  14107  ivthinclemloc  14122  ivthinc  14124  limcimo  14137  limccnp2cntop  14149  dveflem  14190  logbgcd1irrap  14391  lgsdilem  14431  2sqlem5  14469  2sqlem9  14474  qdencn  14778  apdiff  14799