Theorem simprlr 538

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 110	. 2 |- ( ( ps /\ ch ) -> ch )
2	1	ad2antrl 490	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:  imain  5300  fcof1  5786  fliftfun  5799  sbthlemi6  6963  sbthlemi8  6965  addcmpblnq  7368  mulcmpblnq  7369  ordpipqqs  7375  enq0tr  7435  addcmpblnq0  7444  mulcmpblnq0  7445  nnnq0lem1  7447  addnq0mo  7448  mulnq0mo  7449  prarloclemcalc  7503  addlocpr  7537  distrlem4prl  7585  distrlem4pru  7586  addcmpblnr  7740  mulcmpblnrlemg  7741  mulcmpblnr  7742  prsrlem1  7743  addsrmo  7744  mulsrmo  7745  ltsrprg  7748  apreap  8546  apreim  8562  aptap  8609  divdivdivap  8672  divsubdivap  8687  ledivdiv  8849  lediv12a  8853  exbtwnz  10253  seq3caopr  10485  leexp2r  10576  zfz1iso  10823  recvguniq  11006  rsqrmo  11038  summodclem2  11392  prodmodclem2  11587  prodmodc  11588  qredeu  12099  pw2dvdseu  12170  pcadd  12341  mhmpropd  12862  grprcan  12915  isnsg3  13072  ringpropd  13222  islmodd  13388  lmodprop2d  13443  lss1d  13475  epttop  13629  txdis1cn  13817  metequiv2  14035  cncfmptc  14121  cncfmptid  14122  addccncf  14125  negcncf  14127  dedekindicclemicc  14149  2sqlem5  14505  2sqlem9  14510