Theorem simprlr 528

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 482	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  5251  fcof1  5730  fliftfun  5743  sbthlemi6  6903  sbthlemi8  6905  addcmpblnq  7281  mulcmpblnq  7282  ordpipqqs  7288  enq0tr  7348  addcmpblnq0  7357  mulcmpblnq0  7358  nnnq0lem1  7360  addnq0mo  7361  mulnq0mo  7362  prarloclemcalc  7416  addlocpr  7450  distrlem4prl  7498  distrlem4pru  7499  addcmpblnr  7653  mulcmpblnrlemg  7654  mulcmpblnr  7655  prsrlem1  7656  addsrmo  7657  mulsrmo  7658  ltsrprg  7661  apreap  8456  apreim  8472  divdivdivap  8580  divsubdivap  8595  ledivdiv  8755  lediv12a  8759  exbtwnz  10143  seq3caopr  10375  leexp2r  10466  zfz1iso  10705  recvguniq  10888  rsqrmo  10920  summodclem2  11272  prodmodclem2  11467  prodmodc  11468  qredeu  11965  pw2dvdseu  12033  epttop  12461  txdis1cn  12649  metequiv2  12867  cncfmptc  12953  cncfmptid  12954  addccncf  12957  negcncf  12959  dedekindicclemicc  12981