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  6610  tfrcl  6640  nnsucuniel  6773  nntr2  6781  pw2f1odclem  7140  fopwdom  7142  fidceq  7177  fisbth  7193  fidcen  7209  fientri3  7228  unsnfidcex  7233  undifdc  7237  iunfidisj  7266  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  10054  xleadd1a  10291  ixxss12  10324  elfz0ubfz0  10548  qtri3or  10691  exbtwnzlemstep  10698  exbtwnzlemex  10700  exbtwnz  10701  rebtwn2zlemstep  10703  rebtwn2z  10705  btwnzge0  10755  iseqf1olemqf1o  10963  mulexpzap  11036  leexp1a  11051  hashen  11244  fihashdom  11264  hashun  11266  hashf1lem2  11307  swrdccatin1  11518  pfxccatin12lem3  11525  pfxccat3  11527  cjap  11693  cvg1nlemres  11772  rsqrmo  11814  abslt  11876  abs3lem  11899  cau3lem  11902  rexanre  12008  xrmaxltsup  12048  climcau  12137  sumeq2  12149  summodc  12174  fisumss  12183  fsum2d  12226  fsumabs  12256  fsumiun  12268  prodeq2  12348  prodmodclem2  12368  fprodcl2lem  12396  fprodap0  12412  fprod2d  12414  fprodrec  12420  fprodap0f  12427  fprodle  12431  eirrap  12569  divalglemeunn  12712  divalglemeuneg  12714  bezoutlemnewy  12797  bezoutlemstep  12798  bezoutlemmain  12799  bezoutlembi  12806  bezoutlemeu  12808  qredeu  12899  isprm5lem  12944  pwbdvdseu  12971  sqrt2irrap  12984  pythagtriplem2  13073  pythagtrip  13090  pclemub  13094  pcqmul  13110  pcexp  13116  pcneg  13132  pcprmpw2  13140  pcadd  13147  prmpwdvds  13162  4sqlem13m  13210  ballotfilemsf1o  13314  ennnfonelemg  13351  ennnfonelemrnh  13364  ctiunctlemfo  13387  nninfdclemf1  13400  imasival  13685  sgrppropd  13786  ismndd  13808  mndpropd  13811  mhmeql  13857  mhmmnd  13977  mulgfng  13985  issubg4m  14054  ssnmz  14072  conjnmzb  14141  gsumvalfi  14241  rngpropd  14360  ringpropd  14449  dvdsrtr  14516  aprlring  14708  islmod  14735  assapropd  15122  psrbaglefifi  15175  psrbagmax  15183  restbasg  15411  cnpnei  15462  cnptoprest2  15483  cnpdis  15485  lmtopcnp  15493  txcnp  15514  ismet2  15597  blininf  15667  metss2lem  15740  xmettxlem  15752  xmettx  15753  metcnp  15755  metcnpi3  15760  addcncntoplem  15804  fsumcncntop  15810  mulc1cncf  15832  cncfco  15834  mulcncf  15851  dedekindeulemuub  15860  dedekindeu  15866  dedekindicclemuub  15869  ivthinclemloc  15884  ivthinc  15886  limcimo  15908  limccnp2cntop  15920  dveflem  15969  plyf  15980  plyco  16002  plycj  16004  dvply2g  16009  logbgcd1irrap  16223  zprmlogbap  16235  perfectlem2  16317  lgsdilem  16368  lgsquad2lem2  16423  lgsquad3  16425  2sqlem5  16460  2sqlem9  16465  usgredg4  16678  usgr1eop  16708  usgr1vr  16711  subuhgr  16735  subumgr  16737  subusgr  16738  clwwlknonex2lem2  16901  pw1map  17247  qdencn  17295  apdiff  17321  qdiff  17322