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  5983  riota5f  6068  tfrexlem  6609  tfrcl  6639  nnsucuniel  6772  nntr2  6780  pw2f1odclem  7138  fopwdom  7140  fidceq  7175  fisbth  7191  fidcen  7207  fientri3  7226  unsnfidcex  7231  undifdc  7235  iunfidisj  7264  fiuni  7317  2omap  7324  ordiso2  7381  nninfninc  7469  acfun  7569  2omotaplemap  7629  ccfunen  7636  addcmpblnq  7740  mulcmpblnq  7741  ordpipqqs  7747  addcmpblnq0  7816  mulcmpblnq0  7817  prml  7850  addlocpr  7909  prmuloc  7939  mullocpr  7944  ltexprlemopl  7974  ltexprlemopu  7976  ltexprlemloc  7980  ltexprlemrl  7983  ltexprlemru  7985  addcanprleml  7987  addcanprlemu  7988  aptiprleml  8012  ltmprr  8015  cauappcvgprlemopl  8019  cauappcvgprlemopu  8021  cauappcvgprlemloc  8025  caucvgprlemopl  8042  caucvgprlemopu  8044  caucvgprlemloc  8048  caucvgprprlemopu  8072  caucvgprprlemloc  8076  caucvgprprlemexbt  8079  caucvgprprlemaddq  8081  suplocexprlemrl  8090  suplocexprlemdisj  8093  suplocexprlemloc  8094  suplocexprlemub  8096  addcmpblnr  8112  mulcmpblnrlemg  8113  mulcmpblnr  8114  ltsrprg  8120  mulgt0sr  8151  caucvgsrlemgt1  8168  suplocsrlemb  8179  axmulcl  8239  axcaucvglemres  8272  axpre-suploclemres  8274  axpre-suploc  8275  cnegexlem1  8508  negeu  8524  add20  8809  apreap  8923  cru  8938  apsym  8942  apcotr  8943  apadd1  8944  apneg  8947  mulext1  8948  mulge0  8955  mulap0  8990  divdivdivap  9051  prodgt0  9190  ltmul12a  9198  lt2mul2div  9217  ledivdiv  9228  lediv12a  9232  qapne  10055  xleadd1a  10292  ixxss12  10325  elfz0ubfz0  10549  qtri3or  10692  exbtwnzlemstep  10699  exbtwnzlemex  10701  exbtwnz  10702  rebtwn2zlemstep  10704  rebtwn2z  10706  btwnzge0  10756  iseqf1olemqf1o  10964  mulexpzap  11037  leexp1a  11052  hashen  11245  fihashdom  11265  hashun  11267  hashf1lem2  11308  swrdccatin1  11519  pfxccatin12lem3  11526  pfxccat3  11528  cjap  11694  cvg1nlemres  11773  rsqrmo  11815  abslt  11877  abs3lem  11900  cau3lem  11903  rexanre  12009  xrmaxltsup  12049  climcau  12138  sumeq2  12150  summodc  12175  fisumss  12184  fsum2d  12227  fsumabs  12257  fsumiun  12269  prodeq2  12349  prodmodclem2  12369  fprodcl2lem  12397  fprodap0  12413  fprod2d  12415  fprodrec  12421  fprodap0f  12428  fprodle  12432  eirrap  12570  divalglemeunn  12713  divalglemeuneg  12715  bezoutlemnewy  12798  bezoutlemstep  12799  bezoutlemmain  12800  bezoutlembi  12807  bezoutlemeu  12809  qredeu  12900  isprm5lem  12945  pwbdvdseu  12972  sqrt2irrap  12985  pythagtriplem2  13074  pythagtrip  13091  pclemub  13095  pcqmul  13111  pcexp  13117  pcneg  13133  pcprmpw2  13141  pcadd  13148  prmpwdvds  13163  4sqlem13m  13211  ballotfilemsf1o  13315  ennnfonelemg  13352  ennnfonelemrnh  13365  ctiunctlemfo  13388  nninfdclemf1  13401  imasival  13686  sgrppropd  13787  ismndd  13809  mndpropd  13812  mhmeql  13858  mhmmnd  13978  mulgfng  13986  issubg4m  14055  ssnmz  14073  conjnmzb  14142  gsumvalfi  14242  rngpropd  14361  ringpropd  14450  dvdsrtr  14517  aprlring  14709  islmod  14736  assapropd  15123  psrbaglefifi  15172  mplsubgfilemcl  15215  restbasg  15394  cnpnei  15445  cnptoprest2  15466  cnpdis  15468  lmtopcnp  15476  txcnp  15497  ismet2  15580  blininf  15650  metss2lem  15723  xmettxlem  15735  xmettx  15736  metcnp  15738  metcnpi3  15743  addcncntoplem  15787  fsumcncntop  15793  mulc1cncf  15815  cncfco  15817  mulcncf  15834  dedekindeulemuub  15843  dedekindeu  15849  dedekindicclemuub  15852  ivthinclemloc  15867  ivthinc  15869  limcimo  15891  limccnp2cntop  15903  dveflem  15952  plyf  15963  plyco  15985  plycj  15987  dvply2g  15992  logbgcd1irrap  16206  zprmlogbap  16218  perfectlem2  16300  lgsdilem  16351  lgsquad2lem2  16406  lgsquad3  16408  2sqlem5  16443  2sqlem9  16448  usgredg4  16661  usgr1eop  16691  usgr1vr  16694  subuhgr  16718  subumgr  16720  subusgr  16721  clwwlknonex2lem2  16884  pw1map  17230  qdencn  17278  apdiff  17304  qdiff  17305