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  5341  fcof1  5833  mpo0  5996  eroveu  6694  sbthlemi6  7037  sbthlemi8  7039  addcmpblnq  7451  mulcmpblnq  7452  ordpipqqs  7458  addcmpblnq0  7527  mulcmpblnq0  7528  nnnq0lem1  7530  prarloclemcalc  7586  addlocpr  7620  distrlem4prl  7668  distrlem4pru  7669  ltpopr  7679  addcmpblnr  7823  mulcmpblnrlemg  7824  mulcmpblnr  7825  prsrlem1  7826  ltsrprg  7831  apreap  8631  apreim  8647  aptap  8694  divdivdivap  8757  divmuleqap  8761  divadddivap  8771  divsubdivap  8772  ledivdiv  8934  lediv12a  8938  exbtwnz  10357  seq3caopr  10604  seqcaoprg  10605  leexp2r  10702  zfz1iso  10950  recvguniq  11177  rsqrmo  11209  summodclem2  11564  prodmodc  11760  qredeu  12290  pw2dvdseu  12361  pcadd  12534  mhmpropd  13168  issubmd  13176  grprcan  13239  isnsg3  13413  ghmpreima  13472  rngpropd  13587  ringpropd  13670  lmodvsmmulgdi  13955  lmodprop2d  13980  lss1d  14015  epttop  14410  txdis1cn  14598  metequiv2  14816  mulc1cncf  14909  cncfmptc  14916  cncfmptid  14917  addccncf  14920  negcncf  14925  dedekindicclemicc  14952  mpodvdsmulf1o  15310  2sqlem5  15444  2sqlem9  15449