Theorem simprlr 540

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  5419  fcof1  5934  fliftfun  5947  sbthlemi6  7204  sbthlemi8  7206  addcmpblnq  7630  mulcmpblnq  7631  ordpipqqs  7637  enq0tr  7697  addcmpblnq0  7706  mulcmpblnq0  7707  nnnq0lem1  7709  addnq0mo  7710  mulnq0mo  7711  prarloclemcalc  7765  addlocpr  7799  distrlem4prl  7847  distrlem4pru  7848  addcmpblnr  8002  mulcmpblnrlemg  8003  mulcmpblnr  8004  prsrlem1  8005  addsrmo  8006  mulsrmo  8007  ltsrprg  8010  apreap  8810  apreim  8826  aptap  8873  divdivdivap  8936  divsubdivap  8951  ledivdiv  9113  lediv12a  9117  exbtwnz  10554  seq3caopr  10801  seqcaoprg  10802  leexp2r  10899  zfz1iso  11149  wrd2ind  11351  swrdccat  11363  recvguniq  11616  rsqrmo  11648  summodclem2  12004  prodmodclem2  12199  prodmodc  12200  qredeu  12730  pw2dvdseu  12801  pcadd  12974  mhmpropd  13610  grprcan  13681  isnsg3  13855  ghmpreima  13914  rngpropd  14030  ringpropd  14113  islmodd  14369  lmodprop2d  14424  lss1d  14459  epttop  14881  txdis1cn  15069  metequiv2  15287  cncfmptc  15387  cncfmptid  15388  addccncf  15391  negcncf  15396  dedekindicclemicc  15423  mpodvdsmulf1o  15784  2sqlem5  15918  2sqlem9  15923