Theorem simprlr 527

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

Assertion

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

Proof of Theorem simprlr

Step	Hyp	Ref	Expression
1		simpr 109	. 2 |- ( ( ps /\ ch ) -> ch )
2	1	ad2antrl 481	1 |- ( ( ph /\ ( ( ps /\ ch ) /\ th ) ) -> ch )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  imain  5205  fcof1  5684  fliftfun  5697  sbthlemi6  6850  sbthlemi8  6852  addcmpblnq  7178  mulcmpblnq  7179  ordpipqqs  7185  enq0tr  7245  addcmpblnq0  7254  mulcmpblnq0  7255  nnnq0lem1  7257  addnq0mo  7258  mulnq0mo  7259  prarloclemcalc  7313  addlocpr  7347  distrlem4prl  7395  distrlem4pru  7396  addcmpblnr  7550  mulcmpblnrlemg  7551  mulcmpblnr  7552  prsrlem1  7553  addsrmo  7554  mulsrmo  7555  ltsrprg  7558  apreap  8352  apreim  8368  divdivdivap  8476  divsubdivap  8491  ledivdiv  8651  lediv12a  8655  exbtwnz  10031  seq3caopr  10259  leexp2r  10350  zfz1iso  10587  recvguniq  10770  rsqrmo  10802  summodclem2  11154  prodmodclem2  11349  prodmodc  11350  qredeu  11781  pw2dvdseu  11849  epttop  12262  txdis1cn  12450  metequiv2  12668  cncfmptc  12754  cncfmptid  12755  addccncf  12758  negcncf  12760  dedekindicclemicc  12782