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  5300  fcof1  5786  mpo0  5947  eroveu  6628  sbthlemi6  6963  sbthlemi8  6965  addcmpblnq  7368  mulcmpblnq  7369  ordpipqqs  7375  addcmpblnq0  7444  mulcmpblnq0  7445  nnnq0lem1  7447  prarloclemcalc  7503  addlocpr  7537  distrlem4prl  7585  distrlem4pru  7586  ltpopr  7596  addcmpblnr  7740  mulcmpblnrlemg  7741  mulcmpblnr  7742  prsrlem1  7743  ltsrprg  7748  apreap  8546  apreim  8562  aptap  8609  divdivdivap  8672  divmuleqap  8676  divadddivap  8686  divsubdivap  8687  ledivdiv  8849  lediv12a  8853  exbtwnz  10253  seq3caopr  10485  leexp2r  10576  zfz1iso  10823  recvguniq  11006  rsqrmo  11038  summodclem2  11392  prodmodc  11588  qredeu  12099  pw2dvdseu  12170  pcadd  12341  mhmpropd  12862  issubmd  12870  grprcan  12915  isnsg3  13072  ringpropd  13222  lmodvsmmulgdi  13418  lmodprop2d  13443  lss1d  13475  epttop  13675  txdis1cn  13863  metequiv2  14081  mulc1cncf  14161  cncfmptc  14167  cncfmptid  14168  addccncf  14171  negcncf  14173  dedekindicclemicc  14195  2sqlem5  14551  2sqlem9  14556