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  8501  negeu  8517  add20  8802  apreap  8915  cru  8930  apsym  8934  apcotr  8935  apadd1  8936  apneg  8939  mulext1  8940  mulge0  8947  mulap0  8982  divdivdivap  9043  prodgt0  9182  ltmul12a  9190  lt2mul2div  9209  ledivdiv  9220  lediv12a  9224  qapne  10039  xleadd1a  10275  ixxss12  10308  elfz0ubfz0  10532  qtri3or  10675  exbtwnzlemstep  10682  exbtwnzlemex  10684  exbtwnz  10685  rebtwn2zlemstep  10687  rebtwn2z  10689  btwnzge0  10735  iseqf1olemqf1o  10943  mulexpzap  11016  leexp1a  11031  hashen  11223  fihashdom  11243  hashun  11245  hashf1lem2  11286  swrdccatin1  11497  pfxccatin12lem3  11504  pfxccat3  11506  cjap  11672  cvg1nlemres  11751  rsqrmo  11793  abslt  11854  abs3lem  11877  cau3lem  11880  rexanre  11986  xrmaxltsup  12024  climcau  12113  sumeq2  12125  summodc  12150  fisumss  12159  fsum2d  12202  fsumabs  12232  fsumiun  12244  prodeq2  12324  prodmodclem2  12344  fprodcl2lem  12372  fprodap0  12388  fprod2d  12390  fprodrec  12396  fprodap0f  12403  fprodle  12407  eirrap  12545  divalglemeunn  12688  divalglemeuneg  12690  bezoutlemnewy  12773  bezoutlemstep  12774  bezoutlemmain  12775  bezoutlembi  12782  bezoutlemeu  12784  qredeu  12875  isprm5lem  12919  pw2dvdseu  12946  sqrt2irrap  12958  pythagtriplem2  13045  pythagtrip  13062  pclemub  13066  pcqmul  13082  pcexp  13088  pcneg  13104  pcprmpw2  13112  pcadd  13119  prmpwdvds  13134  4sqlem13m  13182  ballotfilemsf1o  13257  ennnfonelemg  13294  ennnfonelemrnh  13307  ctiunctlemfo  13330  nninfdclemf1  13343  imasival  13627  sgrppropd  13728  ismndd  13750  mndpropd  13753  mhmeql  13799  mhmmnd  13919  mulgfng  13927  issubg4m  13996  ssnmz  14014  conjnmzb  14083  gsumvalfi  14152  rngpropd  14254  ringpropd  14343  dvdsrtr  14408  aprlring  14600  islmod  14627  assapropd  15014  mplsubgfilemcl  15090  restbasg  15269  cnpnei  15320  cnptoprest2  15341  cnpdis  15343  lmtopcnp  15351  txcnp  15372  ismet2  15455  blininf  15525  metss2lem  15598  xmettxlem  15610  xmettx  15611  metcnp  15613  metcnpi3  15618  addcncntoplem  15662  fsumcncntop  15668  mulc1cncf  15690  cncfco  15692  mulcncf  15709  dedekindeulemuub  15718  dedekindeu  15724  dedekindicclemuub  15727  ivthinclemloc  15742  ivthinc  15744  limcimo  15766  limccnp2cntop  15778  dveflem  15827  plyf  15838  plyco  15860  plycj  15862  dvply2g  15867  logbgcd1irrap  16072  perfectlem2  16114  lgsdilem  16146  lgsquad2lem2  16201  lgsquad3  16203  2sqlem5  16238  2sqlem9  16243  usgredg4  16456  usgr1eop  16486  usgr1vr  16489  subuhgr  16513  subumgr  16515  subusgr  16516  clwwlknonex2lem2  16679  pw1map  17025  qdencn  17072  apdiff  17097  qdiff  17098