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  3122  disjiun  4077  isotr  5933  riota5f  5974  tfrexlem  6470  tfrcl  6500  nnsucuniel  6631  pw2f1odclem  6983  fopwdom  6985  dif1enen  7030  fisbth  7033  fin0  7035  fin0or  7036  diffisn  7043  finexdc  7052  fientri3  7065  unfidisj  7072  undifdc  7074  ssfirab  7086  fnfi  7091  iunfidisj  7101  dcfi  7136  ordiso2  7190  difinfinf  7256  ctmlemr  7263  exmidfodomrlemr  7368  2omotaplemap  7431  cc2lem  7440  cc3  7442  addcmpblnq  7542  mulcmpblnq  7543  ordpipqqs  7549  ltexnqq  7583  addcmpblnq0  7618  mulcmpblnq0  7619  prmu  7653  addlocpr  7711  prmuloc  7741  prmuloc2  7742  ltaddpr  7772  ltexprlemopl  7776  ltexprlemopu  7778  ltexprlemloc  7782  ltexprlemrl  7785  ltexprlemru  7787  addcanprleml  7789  addcanprlemu  7790  aptiprleml  7814  aptiprlemu  7815  ltmprr  7817  cauappcvgprlemloc  7827  archrecpr  7839  caucvgprlemloc  7850  caucvgprprlemloc  7878  caucvgprprlemexbt  7881  suplocexprlemdisj  7895  suplocexprlemloc  7896  addcmpblnr  7914  mulcmpblnrlemg  7915  mulcmpblnr  7916  ltsrprg  7922  mulgt0sr  7953  caucvgsrlemgt1  7970  suplocsrlemb  7981  axmulcl  8041  axarch  8066  axcaucvglemres  8074  axpre-suploclemres  8076  axpre-suploc  8077  readdcan  8274  cnegexlem1  8309  negeu  8325  add20  8609  apreap  8722  cru  8737  apsym  8741  apcotr  8742  apadd1  8743  apneg  8746  mulext1  8747  divdivdivap  8848  ltmul12a  8995  lemul12a  8997  lt2mul2div  9014  ledivdiv  9025  lediv12a  9029  qapne  9822  xleadd1a  10057  ixxss12  10090  ioodisj  10177  fz0fzelfz0  10311  zsupcllemstep  10436  zsupssdc  10445  qtri3or  10447  exbtwnzlemstep  10454  exbtwnzlemex  10456  exbtwnz  10457  rebtwn2zlemstep  10459  rebtwn2z  10461  qbtwnre  10463  btwnzge0  10507  iseqf1olemqf1o  10715  mulexpzap  10788  leexp1a  10803  expnbnd  10872  hashen  10993  fihashdom  11012  hashun  11014  zfz1iso  11050  swrdccat  11253  reuccatpfxs1  11265  cjap  11403  cvg1nlemres  11482  rsqrmo  11524  abs3lem  11608  cau3lem  11611  rexanre  11717  xrmaxltsup  11755  climcau  11844  sumeq2  11856  summodc  11880  fsum3cvg3  11893  fsum2d  11932  prodeq2  12054  prodmodclem2  12074  fprod2d  12120  eirrap  12275  addmodlteqALT  12356  divalglemeunn  12418  divalglemeuneg  12420  bezoutlemnewy  12503  bezoutlemstep  12504  bezoutlemmain  12505  bezoutlembi  12512  bezoutlemeu  12514  rpdvds  12607  isprm5lem  12649  isprm6  12655  pw2dvdslemn  12673  pw2dvdseu  12676  sqrt2irrap  12688  pythagtriplem2  12775  pythagtrip  12792  pclemub  12796  pcqmul  12812  pcexp  12818  pcneg  12834  pcprmpw2  12842  pcadd  12849  pcmpt  12852  4sqlem13m  12912  ennnfonelemrnh  12973  ennnfonelemnn0  12979  ctinfomlemom  12984  ctiunctlemfo  12996  nninfdclemf1  13009  imasival  13325  gsumpropd2  13412  sgrppropd  13432  ismndd  13456  mndpropd  13459  mhmeql  13511  mhmmnd  13639  issubg4m  13716  ssnmz  13734  conjnmzb  13803  rngpropd  13904  ringpropd  13987  islmod  14240  psrval  14615  restbasg  14827  cnrest2  14895  cnpdis  14901  lmtopcnp  14909  txcnp  14930  txlm  14938  ismet2  15013  blininf  15083  metss2lem  15156  xmettxlem  15168  xmettx  15169  metcnp3  15170  metcnpi3  15176  addcncntoplem  15220  fsumcncntop  15226  mulcncf  15267  dedekindeulemuub  15276  dedekindeu  15282  dedekindicclemuub  15285  ivthinclemlopn  15295  ivthinclemuopn  15297  ivthinclemloc  15300  ivthinc  15302  ivthdichlem  15310  limcimo  15324  limccnp2cntop  15336  plyf  15396  plyco  15418  plycj  15420  plyrecj  15422  dvply2g  15425  logbgcd1irrap  15629  perfectlem2  15659  lgsdilem  15691  lgsquad2lem2  15746  lgsquad3  15748  2sqlem5  15783  2sqlem9  15788  usgredg4  15998  2omap  16290  qdencn  16326  apdiff  16347