Theorem simplrl 541

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 493	1 |- ( ( ( ph /\ ( ps /\ ch ) ) /\ th ) -> ps )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  rmob  3145  disjiun  4125  f1imass  5980  riota5f  6065  tfrexlem  6605  tfrcl  6635  nnsucuniel  6768  nntr2  6776  pw2f1odclem  7134  fopwdom  7136  fidceq  7171  fisbth  7187  fidcen  7203  fientri3  7222  unsnfidcex  7227  undifdc  7231  iunfidisj  7260  fiuni  7312  2omap  7318  ordiso2  7375  nninfninc  7463  acfun  7563  2omotaplemap  7623  ccfunen  7630  addcmpblnq  7734  mulcmpblnq  7735  ordpipqqs  7741  addcmpblnq0  7810  mulcmpblnq0  7811  prml  7844  addlocpr  7903  prmuloc  7933  mullocpr  7938  ltexprlemopl  7968  ltexprlemopu  7970  ltexprlemloc  7974  ltexprlemrl  7977  ltexprlemru  7979  addcanprleml  7981  addcanprlemu  7982  aptiprleml  8006  ltmprr  8009  cauappcvgprlemopl  8013  cauappcvgprlemopu  8015  cauappcvgprlemloc  8019  caucvgprlemopl  8036  caucvgprlemopu  8038  caucvgprlemloc  8042  caucvgprprlemopu  8066  caucvgprprlemloc  8070  caucvgprprlemexbt  8073  caucvgprprlemaddq  8075  suplocexprlemrl  8084  suplocexprlemdisj  8087  suplocexprlemloc  8088  suplocexprlemub  8090  addcmpblnr  8106  mulcmpblnrlemg  8107  mulcmpblnr  8108  ltsrprg  8114  mulgt0sr  8145  caucvgsrlemgt1  8162  suplocsrlemb  8173  axmulcl  8233  axcaucvglemres  8266  axpre-suploclemres  8268  axpre-suploc  8269  cnegexlem1  8502  negeu  8518  add20  8803  apreap  8917  cru  8932  apsym  8936  apcotr  8937  apadd1  8938  apneg  8941  mulext1  8942  mulge0  8949  mulap0  8984  divdivdivap  9045  prodgt0  9184  ltmul12a  9192  lt2mul2div  9211  ledivdiv  9222  lediv12a  9226  qapne  10048  xleadd1a  10285  ixxss12  10318  elfz0ubfz0  10542  qtri3or  10685  exbtwnzlemstep  10692  exbtwnzlemex  10694  exbtwnz  10695  rebtwn2zlemstep  10697  rebtwn2z  10699  btwnzge0  10748  iseqf1olemqf1o  10956  mulexpzap  11029  leexp1a  11044  hashen  11237  fihashdom  11257  hashun  11259  hashf1lem2  11300  swrdccatin1  11511  pfxccatin12lem3  11518  pfxccat3  11520  cjap  11686  cvg1nlemres  11765  rsqrmo  11807  abslt  11869  abs3lem  11892  cau3lem  11895  rexanre  12001  xrmaxltsup  12040  climcau  12129  sumeq2  12141  summodc  12166  fisumss  12175  fsum2d  12218  fsumabs  12248  fsumiun  12260  prodeq2  12340  prodmodclem2  12360  fprodcl2lem  12388  fprodap0  12404  fprod2d  12406  fprodrec  12412  fprodap0f  12419  fprodle  12423  eirrap  12561  divalglemeunn  12704  divalglemeuneg  12706  bezoutlemnewy  12789  bezoutlemstep  12790  bezoutlemmain  12791  bezoutlembi  12798  bezoutlemeu  12800  qredeu  12891  isprm5lem  12936  pwbdvdseu  12963  sqrt2irrap  12976  pythagtriplem2  13065  pythagtrip  13082  pclemub  13086  pcqmul  13102  pcexp  13108  pcneg  13124  pcprmpw2  13132  pcadd  13139  prmpwdvds  13154  4sqlem13m  13202  ballotfilemsf1o  13306  ennnfonelemg  13343  ennnfonelemrnh  13356  ctiunctlemfo  13379  nninfdclemf1  13392  imasival  13676  sgrppropd  13777  ismndd  13799  mndpropd  13802  mhmeql  13848  mhmmnd  13968  mulgfng  13976  issubg4m  14045  ssnmz  14063  conjnmzb  14132  gsumvalfi  14201  rngpropd  14303  ringpropd  14392  dvdsrtr  14457  aprlring  14649  islmod  14676  assapropd  15063  mplsubgfilemcl  15139  restbasg  15318  cnpnei  15369  cnptoprest2  15390  cnpdis  15392  lmtopcnp  15400  txcnp  15421  ismet2  15504  blininf  15574  metss2lem  15647  xmettxlem  15659  xmettx  15660  metcnp  15662  metcnpi3  15667  addcncntoplem  15711  fsumcncntop  15717  mulc1cncf  15739  cncfco  15741  mulcncf  15758  dedekindeulemuub  15767  dedekindeu  15773  dedekindicclemuub  15776  ivthinclemloc  15791  ivthinc  15793  limcimo  15815  limccnp2cntop  15827  dveflem  15876  plyf  15887  plyco  15909  plycj  15911  dvply2g  15916  logbgcd1irrap  16125  zprmlogbap  16137  perfectlem2  16198  lgsdilem  16244  lgsquad2lem2  16299  lgsquad3  16301  2sqlem5  16336  2sqlem9  16341  usgredg4  16554  usgr1eop  16584  usgr1vr  16587  subuhgr  16611  subumgr  16613  subusgr  16614  clwwlknonex2lem2  16777  pw1map  17123  qdencn  17170  apdiff  17195  qdiff  17196