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  5412  fcof1  5924  fliftfun  5937  sbthlemi6  7161  sbthlemi8  7163  addcmpblnq  7587  mulcmpblnq  7588  ordpipqqs  7594  enq0tr  7654  addcmpblnq0  7663  mulcmpblnq0  7664  nnnq0lem1  7666  addnq0mo  7667  mulnq0mo  7668  prarloclemcalc  7722  addlocpr  7756  distrlem4prl  7804  distrlem4pru  7805  addcmpblnr  7959  mulcmpblnrlemg  7960  mulcmpblnr  7961  prsrlem1  7962  addsrmo  7963  mulsrmo  7964  ltsrprg  7967  apreap  8767  apreim  8783  aptap  8830  divdivdivap  8893  divsubdivap  8908  ledivdiv  9070  lediv12a  9074  exbtwnz  10510  seq3caopr  10757  seqcaoprg  10758  leexp2r  10855  zfz1iso  11105  wrd2ind  11304  swrdccat  11316  recvguniq  11556  rsqrmo  11588  summodclem2  11944  prodmodclem2  12139  prodmodc  12140  qredeu  12670  pw2dvdseu  12741  pcadd  12914  mhmpropd  13550  grprcan  13621  isnsg3  13795  ghmpreima  13854  rngpropd  13970  ringpropd  14053  islmodd  14309  lmodprop2d  14364  lss1d  14399  epttop  14816  txdis1cn  15004  metequiv2  15222  cncfmptc  15322  cncfmptid  15323  addccncf  15326  negcncf  15331  dedekindicclemicc  15358  mpodvdsmulf1o  15716  2sqlem5  15850  2sqlem9  15855