Theorem simprll 532

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 487	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  5280  fcof1  5762  mpo0  5923  eroveu  6604  sbthlemi6  6939  sbthlemi8  6941  addcmpblnq  7329  mulcmpblnq  7330  ordpipqqs  7336  addcmpblnq0  7405  mulcmpblnq0  7406  nnnq0lem1  7408  prarloclemcalc  7464  addlocpr  7498  distrlem4prl  7546  distrlem4pru  7547  ltpopr  7557  addcmpblnr  7701  mulcmpblnrlemg  7702  mulcmpblnr  7703  prsrlem1  7704  ltsrprg  7709  apreap  8506  apreim  8522  divdivdivap  8630  divmuleqap  8634  divadddivap  8644  divsubdivap  8645  ledivdiv  8806  lediv12a  8810  exbtwnz  10207  seq3caopr  10439  leexp2r  10530  zfz1iso  10776  recvguniq  10959  rsqrmo  10991  summodclem2  11345  prodmodc  11541  qredeu  12051  pw2dvdseu  12122  pcadd  12293  mhmpropd  12689  issubmd  12696  grprcan  12740  epttop  12884  txdis1cn  13072  metequiv2  13290  mulc1cncf  13370  cncfmptc  13376  cncfmptid  13377  addccncf  13380  negcncf  13382  dedekindicclemicc  13404  2sqlem5  13749  2sqlem9  13754