Theorem simplrl 537

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  3139  disjiun  4110  f1imass  5954  riota5f  6039  tfrexlem  6579  tfrcl  6609  nnsucuniel  6742  nntr2  6750  pw2f1odclem  7101  fopwdom  7103  fidceq  7138  fisbth  7154  fidcen  7170  fientri3  7189  unsnfidcex  7194  undifdc  7198  iunfidisj  7227  fiuni  7279  2omap  7283  ordiso2  7340  nninfninc  7428  acfun  7528  2omotaplemap  7588  ccfunen  7595  addcmpblnq  7699  mulcmpblnq  7700  ordpipqqs  7706  addcmpblnq0  7775  mulcmpblnq0  7776  prml  7809  addlocpr  7868  prmuloc  7898  mullocpr  7903  ltexprlemopl  7933  ltexprlemopu  7935  ltexprlemloc  7939  ltexprlemrl  7942  ltexprlemru  7944  addcanprleml  7946  addcanprlemu  7947  aptiprleml  7971  ltmprr  7974  cauappcvgprlemopl  7978  cauappcvgprlemopu  7980  cauappcvgprlemloc  7984  caucvgprlemopl  8001  caucvgprlemopu  8003  caucvgprlemloc  8007  caucvgprprlemopu  8031  caucvgprprlemloc  8035  caucvgprprlemexbt  8038  caucvgprprlemaddq  8040  suplocexprlemrl  8049  suplocexprlemdisj  8052  suplocexprlemloc  8053  suplocexprlemub  8055  addcmpblnr  8071  mulcmpblnrlemg  8072  mulcmpblnr  8073  ltsrprg  8079  mulgt0sr  8110  caucvgsrlemgt1  8127  suplocsrlemb  8138  axmulcl  8198  axcaucvglemres  8231  axpre-suploclemres  8233  axpre-suploc  8234  cnegexlem1  8466  negeu  8482  add20  8767  apreap  8880  cru  8895  apsym  8899  apcotr  8900  apadd1  8901  apneg  8904  mulext1  8905  mulge0  8912  mulap0  8947  divdivdivap  9008  prodgt0  9147  ltmul12a  9155  lt2mul2div  9174  ledivdiv  9185  lediv12a  9189  qapne  9993  xleadd1a  10229  ixxss12  10262  elfz0ubfz0  10485  qtri3or  10628  exbtwnzlemstep  10635  exbtwnzlemex  10637  exbtwnz  10638  rebtwn2zlemstep  10640  rebtwn2z  10642  btwnzge0  10688  iseqf1olemqf1o  10896  mulexpzap  10969  leexp1a  10984  hashen  11176  fihashdom  11196  hashun  11198  swrdccatin1  11446  pfxccatin12lem3  11453  pfxccat3  11455  cjap  11621  cvg1nlemres  11700  rsqrmo  11742  abslt  11803  abs3lem  11826  cau3lem  11829  rexanre  11935  xrmaxltsup  11973  climcau  12062  sumeq2  12074  summodc  12099  fisumss  12108  fsum2d  12151  fsumabs  12181  fsumiun  12193  prodeq2  12273  prodmodclem2  12293  fprodcl2lem  12321  fprodap0  12337  fprod2d  12339  fprodrec  12345  fprodap0f  12352  fprodle  12356  eirrap  12494  divalglemeunn  12637  divalglemeuneg  12639  bezoutlemnewy  12722  bezoutlemstep  12723  bezoutlemmain  12724  bezoutlembi  12731  bezoutlemeu  12733  qredeu  12824  isprm5lem  12868  pw2dvdseu  12895  sqrt2irrap  12907  pythagtriplem2  12994  pythagtrip  13011  pclemub  13015  pcqmul  13031  pcexp  13037  pcneg  13053  pcprmpw2  13061  pcadd  13068  prmpwdvds  13083  4sqlem13m  13131  ballotfilemsf1o  13206  ennnfonelemg  13243  ennnfonelemrnh  13256  ctiunctlemfo  13279  nninfdclemf1  13292  imasival  13575  sgrppropd  13681  ismndd  13703  mndpropd  13706  mhmeql  13752  mhmmnd  13874  mulgfng  13882  issubg4m  13951  ssnmz  13969  conjnmzb  14038  gfsumval  14107  rngpropd  14199  ringpropd  14286  dvdsrtr  14351  aprlring  14543  islmod  14570  mplsubgfilemcl  14985  restbasg  15164  cnpnei  15215  cnptoprest2  15236  cnpdis  15238  lmtopcnp  15246  txcnp  15267  ismet2  15350  blininf  15420  metss2lem  15493  xmettxlem  15505  xmettx  15506  metcnp  15508  metcnpi3  15513  addcncntoplem  15557  fsumcncntop  15563  mulc1cncf  15585  cncfco  15587  mulcncf  15604  dedekindeulemuub  15613  dedekindeu  15619  dedekindicclemuub  15622  ivthinclemloc  15637  ivthinc  15639  limcimo  15661  limccnp2cntop  15673  dveflem  15722  plyf  15733  plyco  15755  plycj  15757  dvply2g  15762  logbgcd1irrap  15966  perfectlem2  15999  lgsdilem  16031  lgsquad2lem2  16086  lgsquad3  16088  2sqlem5  16123  2sqlem9  16128  usgredg4  16341  usgr1eop  16371  usgr1vr  16374  subuhgr  16398  subumgr  16400  subusgr  16401  clwwlknonex2lem2  16564  pw1map  16910  qdencn  16948  apdiff  16973  qdiff  16974