Theorem simplrr 536

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

Assertion

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

Proof of Theorem simplrr

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

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  3079  disjiun  4025  isotr  5860  riota5f  5899  tfrexlem  6389  tfrcl  6419  nnsucuniel  6550  pw2f1odclem  6892  fopwdom  6894  dif1enen  6938  fisbth  6941  fin0  6943  fin0or  6944  diffisn  6951  finexdc  6960  fientri3  6973  unfidisj  6980  undifdc  6982  ssfirab  6992  fnfi  6997  iunfidisj  7007  dcfi  7042  ordiso2  7096  difinfinf  7162  ctmlemr  7169  exmidfodomrlemr  7264  2omotaplemap  7319  cc2lem  7328  cc3  7330  addcmpblnq  7429  mulcmpblnq  7430  ordpipqqs  7436  ltexnqq  7470  addcmpblnq0  7505  mulcmpblnq0  7506  prmu  7540  addlocpr  7598  prmuloc  7628  prmuloc2  7629  ltaddpr  7659  ltexprlemopl  7663  ltexprlemopu  7665  ltexprlemloc  7669  ltexprlemrl  7672  ltexprlemru  7674  addcanprleml  7676  addcanprlemu  7677  aptiprleml  7701  aptiprlemu  7702  ltmprr  7704  cauappcvgprlemloc  7714  archrecpr  7726  caucvgprlemloc  7737  caucvgprprlemloc  7765  caucvgprprlemexbt  7768  suplocexprlemdisj  7782  suplocexprlemloc  7783  addcmpblnr  7801  mulcmpblnrlemg  7802  mulcmpblnr  7803  ltsrprg  7809  mulgt0sr  7840  caucvgsrlemgt1  7857  suplocsrlemb  7868  axmulcl  7928  axarch  7953  axcaucvglemres  7961  axpre-suploclemres  7963  axpre-suploc  7964  readdcan  8161  cnegexlem1  8196  negeu  8212  add20  8495  apreap  8608  cru  8623  apsym  8627  apcotr  8628  apadd1  8629  apneg  8632  mulext1  8633  divdivdivap  8734  ltmul12a  8881  lemul12a  8883  lt2mul2div  8900  ledivdiv  8911  lediv12a  8915  qapne  9707  xleadd1a  9942  ixxss12  9975  ioodisj  10062  fz0fzelfz0  10196  qtri3or  10313  exbtwnzlemstep  10319  exbtwnzlemex  10321  exbtwnz  10322  rebtwn2zlemstep  10324  rebtwn2z  10326  qbtwnre  10328  btwnzge0  10372  iseqf1olemqf1o  10580  mulexpzap  10653  leexp1a  10668  expnbnd  10737  hashen  10858  fihashdom  10877  hashun  10879  zfz1iso  10915  cjap  11053  cvg1nlemres  11132  rsqrmo  11174  abs3lem  11258  cau3lem  11261  rexanre  11367  xrmaxltsup  11404  climcau  11493  sumeq2  11505  summodc  11529  fsum3cvg3  11542  fsum2d  11581  prodeq2  11703  prodmodclem2  11723  fprod2d  11769  eirrap  11924  addmodlteqALT  12004  divalglemeunn  12065  divalglemeuneg  12067  zsupcllemstep  12085  zsupssdc  12094  bezoutlemnewy  12136  bezoutlemstep  12137  bezoutlemmain  12138  bezoutlembi  12145  bezoutlemeu  12147  rpdvds  12240  isprm5lem  12282  isprm6  12288  pw2dvdslemn  12306  pw2dvdseu  12309  sqrt2irrap  12321  pythagtriplem2  12407  pythagtrip  12424  pclemub  12428  pcqmul  12444  pcexp  12450  pcneg  12466  pcprmpw2  12474  pcadd  12481  pcmpt  12484  4sqlem13m  12544  ennnfonelemrnh  12576  ennnfonelemnn0  12582  ctinfomlemom  12587  ctiunctlemfo  12599  nninfdclemf1  12612  imasival  12892  gsumpropd2  12979  sgrppropd  12999  ismndd  13021  mndpropd  13024  mhmeql  13067  mhmmnd  13189  issubg4m  13266  ssnmz  13284  conjnmzb  13353  rngpropd  13454  ringpropd  13537  islmod  13790  psrval  14163  restbasg  14347  cnrest2  14415  cnpdis  14421  lmtopcnp  14429  txcnp  14450  txlm  14458  ismet2  14533  blininf  14603  metss2lem  14676  xmettxlem  14688  xmettx  14689  metcnp3  14690  metcnpi3  14696  addcncntoplem  14740  fsumcncntop  14746  mulcncf  14787  dedekindeulemuub  14796  dedekindeu  14802  dedekindicclemuub  14805  ivthinclemlopn  14815  ivthinclemuopn  14817  ivthinclemloc  14820  ivthinc  14822  ivthdichlem  14830  limcimo  14844  limccnp2cntop  14856  plyf  14916  plyco  14937  plycj  14939  plyrecj  14941  logbgcd1irrap  15143  lgsdilem  15184  lgsquad2lem2  15239  lgsquad3  15241  2sqlem5  15276  2sqlem9  15281  qdencn  15587  apdiff  15608