Theorem simprll 537

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 109	. 2 |- ( ( ps /\ ch ) -> ps )
2	1	ad2antrl 490	1 |- ( ( ph /\ ( ( ps /\ ch ) /\ th ) ) -> ps )

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  5298  fcof1  5783  mpo0  5944  eroveu  6625  sbthlemi6  6960  sbthlemi8  6962  addcmpblnq  7365  mulcmpblnq  7366  ordpipqqs  7372  addcmpblnq0  7441  mulcmpblnq0  7442  nnnq0lem1  7444  prarloclemcalc  7500  addlocpr  7534  distrlem4prl  7582  distrlem4pru  7583  ltpopr  7593  addcmpblnr  7737  mulcmpblnrlemg  7738  mulcmpblnr  7739  prsrlem1  7740  ltsrprg  7745  apreap  8542  apreim  8558  aptap  8605  divdivdivap  8668  divmuleqap  8672  divadddivap  8682  divsubdivap  8683  ledivdiv  8845  lediv12a  8849  exbtwnz  10248  seq3caopr  10480  leexp2r  10571  zfz1iso  10816  recvguniq  10999  rsqrmo  11031  summodclem2  11385  prodmodc  11581  qredeu  12091  pw2dvdseu  12162  pcadd  12333  mhmpropd  12811  issubmd  12819  grprcan  12864  isnsg3  13020  ringpropd  13170  epttop  13483  txdis1cn  13671  metequiv2  13889  mulc1cncf  13969  cncfmptc  13975  cncfmptid  13976  addccncf  13979  negcncf  13981  dedekindicclemicc  14003  2sqlem5  14348  2sqlem9  14353