Theorem simprll 527

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simprll	|- ( ( ph /\ ( ( ps /\ ch ) /\ th ) ) -> ps )

Proof of Theorem simprll

Step	Hyp	Ref	Expression
1		simpl 108	. 2 |- ( ( ps /\ ch ) -> ps )
2	1	ad2antrl 482	1 |- ( ( ph /\ ( ( ps /\ ch ) /\ th ) ) -> ps )

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  5270  fcof1  5751  mpo0  5912  eroveu  6592  sbthlemi6  6927  sbthlemi8  6929  addcmpblnq  7308  mulcmpblnq  7309  ordpipqqs  7315  addcmpblnq0  7384  mulcmpblnq0  7385  nnnq0lem1  7387  prarloclemcalc  7443  addlocpr  7477  distrlem4prl  7525  distrlem4pru  7526  ltpopr  7536  addcmpblnr  7680  mulcmpblnrlemg  7681  mulcmpblnr  7682  prsrlem1  7683  ltsrprg  7688  apreap  8485  apreim  8501  divdivdivap  8609  divmuleqap  8613  divadddivap  8623  divsubdivap  8624  ledivdiv  8785  lediv12a  8789  exbtwnz  10186  seq3caopr  10418  leexp2r  10509  zfz1iso  10754  recvguniq  10937  rsqrmo  10969  summodclem2  11323  prodmodc  11519  qredeu  12029  pw2dvdseu  12100  pcadd  12271  epttop  12740  txdis1cn  12928  metequiv2  13146  mulc1cncf  13226  cncfmptc  13232  cncfmptid  13233  addccncf  13236  negcncf  13238  dedekindicclemicc  13260  2sqlem5  13605  2sqlem9  13610