Theorem simplrr 542

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 493	1 |- ( ( ( ph /\ ( ps /\ ch ) ) /\ th ) -> ch )

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  isotr  6022  riota5f  6065  tfrexlem  6605  tfrcl  6635  nnsucuniel  6768  pw2f1odclem  7134  fopwdom  7136  dif1enen  7184  fisbth  7187  fin0  7189  fin0or  7190  diffisn  7197  fidcen  7203  finexdc  7207  elssdc  7209  fientri3  7222  unfidisj  7229  undifdc  7231  ssfirab  7244  fnfi  7250  iunfidisj  7260  mapfi  7261  fissfi  7263  dcfi  7315  2omap  7319  ordiso2  7376  difinfinf  7442  ctmlemr  7449  exmidfodomrlemr  7555  2omotaplemap  7624  cc2lem  7633  cc3  7635  addcmpblnq  7735  mulcmpblnq  7736  ordpipqqs  7742  ltexnqq  7776  addcmpblnq0  7811  mulcmpblnq0  7812  prmu  7846  addlocpr  7904  prmuloc  7934  prmuloc2  7935  ltaddpr  7965  ltexprlemopl  7969  ltexprlemopu  7971  ltexprlemloc  7975  ltexprlemrl  7978  ltexprlemru  7980  addcanprleml  7982  addcanprlemu  7983  aptiprleml  8007  aptiprlemu  8008  ltmprr  8010  cauappcvgprlemloc  8020  archrecpr  8032  caucvgprlemloc  8043  caucvgprprlemloc  8071  caucvgprprlemexbt  8074  suplocexprlemdisj  8088  suplocexprlemloc  8089  addcmpblnr  8107  mulcmpblnrlemg  8108  mulcmpblnr  8109  ltsrprg  8115  mulgt0sr  8146  caucvgsrlemgt1  8163  suplocsrlemb  8174  axmulcl  8234  axarch  8259  axcaucvglemres  8267  axpre-suploclemres  8269  axpre-suploc  8270  readdcan  8468  cnegexlem1  8503  negeu  8519  add20  8804  apreap  8918  cru  8933  apsym  8937  apcotr  8938  apadd1  8939  apneg  8942  mulext1  8943  divdivdivap  9046  ltmul12a  9193  lemul12a  9195  lt2mul2div  9212  ledivdiv  9223  lediv12a  9227  qapne  10049  xleadd1a  10286  ixxss12  10319  ioodisj  10406  fz0fzelfz0  10545  zsupcllemstep  10673  zsupssdc  10684  qtri3or  10686  exbtwnzlemstep  10693  exbtwnzlemex  10695  exbtwnz  10696  rebtwn2zlemstep  10698  rebtwn2z  10700  qbtwnre  10702  btwnzge0  10749  iseqf1olemqf1o  10957  mulexpzap  11030  leexp1a  11045  expnbnd  11115  hashen  11238  fihashdom  11258  hashun  11260  hashf1  11302  zfz1iso  11308  swrdccat  11522  reuccatpfxs1  11534  cjap  11687  cvg1nlemres  11766  rsqrmo  11808  abs3lem  11893  cau3lem  11896  rexanre  12002  fiidxsupcl  12011  xrmaxltsup  12042  climcau  12131  sumeq2  12143  summodc  12168  fsum3cvg3  12181  fsum2d  12220  prodeq2  12342  prodmodclem2  12362  fprod2d  12408  eirrap  12563  addmodlteqALT  12644  divalglemeunn  12706  divalglemeuneg  12708  bezoutlemnewy  12791  bezoutlemstep  12792  bezoutlemmain  12793  bezoutlembi  12800  bezoutlemeu  12802  rpdvds  12895  isprm5lem  12938  isprm6  12944  pwbdvdslemn  12962  pwbdvdseu  12965  sqrt2irrap  12978  pythagtriplem2  13067  pythagtrip  13084  pclemub  13088  pcqmul  13104  pcexp  13110  pcneg  13126  pcprmpw2  13134  pcadd  13141  pcmpt  13144  4sqlem13m  13204  ballotfilemcdc  13274  ballotfilemfc0  13283  ballotfilemfcc  13284  ennnfonelemrnh  13358  ennnfonelemnn0  13364  ctinfomlemom  13369  ctiunctlemfo  13381  nninfdclemf1  13394  imasival  13678  sgrppropd  13779  ismndd  13801  mndpropd  13804  mhmeql  13850  mhmmnd  13970  issubg4m  14047  ssnmz  14065  conjnmzb  14134  gsumvalfi  14203  rngpropd  14305  ringpropd  14394  aprlring  14651  islmod  14678  assapropd  15065  psrval  15101  psrbaglefifi  15114  restbasg  15321  cnrest2  15389  cnpdis  15395  lmtopcnp  15403  txcnp  15424  txlm  15432  ismet2  15507  blininf  15577  metss2lem  15650  xmettxlem  15662  xmettx  15663  metcnp3  15664  metcnpi3  15670  addcncntoplem  15714  fsumcncntop  15720  mulcncf  15761  dedekindeulemuub  15770  dedekindeu  15776  dedekindicclemuub  15779  ivthinclemlopn  15789  ivthinclemuopn  15791  ivthinclemloc  15794  ivthinc  15796  ivthdichlem  15804  limcimo  15818  limccnp2cntop  15830  plyf  15890  plyco  15912  plycj  15914  plyrecj  15916  dvply2g  15919  logdivlt  16049  logbgcd1irrap  16128  zprmlogbap  16140  perfectlem2  16222  lgsdilem  16268  lgsquad2lem2  16323  lgsquad3  16325  2sqlem5  16360  2sqlem9  16365  usgredg4  16578  usgr1vr  16611  subuhgr  16635  subumgr  16637  clwwlknonex2lem2  16801  eupth2lemsfi  16841  depindlem3  16871  qdencn  17194  apdiff  17219  qdiff  17220