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  5409  fcof1  5919  mpo0  6086  eroveu  6790  sbthlemi6  7152  sbthlemi8  7154  addcmpblnq  7577  mulcmpblnq  7578  ordpipqqs  7584  addcmpblnq0  7653  mulcmpblnq0  7654  nnnq0lem1  7656  prarloclemcalc  7712  addlocpr  7746  distrlem4prl  7794  distrlem4pru  7795  ltpopr  7805  addcmpblnr  7949  mulcmpblnrlemg  7950  mulcmpblnr  7951  prsrlem1  7952  ltsrprg  7957  apreap  8757  apreim  8773  aptap  8820  divdivdivap  8883  divmuleqap  8887  divadddivap  8897  divsubdivap  8898  ledivdiv  9060  lediv12a  9064  exbtwnz  10500  seq3caopr  10747  seqcaoprg  10748  leexp2r  10845  zfz1iso  11095  ccatsymb  11169  wrd2ind  11294  swrdccat  11306  recvguniq  11546  rsqrmo  11578  summodclem2  11933  prodmodc  12129  qredeu  12659  pw2dvdseu  12730  pcadd  12903  mhmpropd  13539  issubmd  13547  grprcan  13610  isnsg3  13784  ghmpreima  13843  rngpropd  13958  ringpropd  14041  lmodvsmmulgdi  14327  lmodprop2d  14352  lss1d  14387  epttop  14804  txdis1cn  14992  metequiv2  15210  mulc1cncf  15303  cncfmptc  15310  cncfmptid  15311  addccncf  15314  negcncf  15319  dedekindicclemicc  15346  mpodvdsmulf1o  15704  2sqlem5  15838  2sqlem9  15843