Theorem simprll 509

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 479	1 |- ( ( ph /\ ( ( ps /\ ch ) /\ th ) ) -> ps )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  imain  5161  fcof1  5636  mpo0  5793  eroveu  6472  sbthlemi6  6800  sbthlemi8  6802  addcmpblnq  7117  mulcmpblnq  7118  ordpipqqs  7124  addcmpblnq0  7193  mulcmpblnq0  7194  nnnq0lem1  7196  prarloclemcalc  7252  addlocpr  7286  distrlem4prl  7334  distrlem4pru  7335  ltpopr  7345  addcmpblnr  7476  mulcmpblnrlemg  7477  mulcmpblnr  7478  prsrlem1  7479  ltsrprg  7484  apreap  8261  apreim  8277  divdivdivap  8380  divmuleqap  8384  divadddivap  8394  divsubdivap  8395  ledivdiv  8552  lediv12a  8556  exbtwnz  9915  seq3caopr  10143  leexp2r  10234  zfz1iso  10471  recvguniq  10653  rsqrmo  10685  summodclem2  11037  qredeu  11618  pw2dvdseu  11685  epttop  12096  txdis1cn  12283  metequiv2  12479  mulc1cncf  12556  cncfmptc  12562  cncfmptid  12563  addccncf  12566  negcncf  12568