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  5362  fcof1  5862  fliftfun  5875  sbthlemi6  7076  sbthlemi8  7078  addcmpblnq  7493  mulcmpblnq  7494  ordpipqqs  7500  enq0tr  7560  addcmpblnq0  7569  mulcmpblnq0  7570  nnnq0lem1  7572  addnq0mo  7573  mulnq0mo  7574  prarloclemcalc  7628  addlocpr  7662  distrlem4prl  7710  distrlem4pru  7711  addcmpblnr  7865  mulcmpblnrlemg  7866  mulcmpblnr  7867  prsrlem1  7868  addsrmo  7869  mulsrmo  7870  ltsrprg  7873  apreap  8673  apreim  8689  aptap  8736  divdivdivap  8799  divsubdivap  8814  ledivdiv  8976  lediv12a  8980  exbtwnz  10406  seq3caopr  10653  seqcaoprg  10654  leexp2r  10751  zfz1iso  10999  recvguniq  11356  rsqrmo  11388  summodclem2  11743  prodmodclem2  11938  prodmodc  11939  qredeu  12469  pw2dvdseu  12540  pcadd  12713  mhmpropd  13348  grprcan  13419  isnsg3  13593  ghmpreima  13652  rngpropd  13767  ringpropd  13850  islmodd  14105  lmodprop2d  14160  lss1d  14195  epttop  14612  txdis1cn  14800  metequiv2  15018  cncfmptc  15118  cncfmptid  15119  addccncf  15122  negcncf  15127  dedekindicclemicc  15154  mpodvdsmulf1o  15512  2sqlem5  15646  2sqlem9  15651