Theorem simprrl 529

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simprrl	|- ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) -> ch )

Proof of Theorem simprrl

Step	Hyp	Ref	Expression
1		simpl 108	. 2 |- ( ( ch /\ th ) -> ch )
2	1	ad2antll 483	1 |- ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) -> ch )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  dn1dc  945  imain  5252  grpridd  6017  tfrlemisucaccv  6272  tfrexlem  6281  tfr1onlemsucaccv  6288  tfrcllemsucaccv  6301  eroveu  6571  addcmpblnq  7287  mulcmpblnq  7288  ordpipqqs  7294  nqnq0pi  7358  addcmpblnq0  7363  mulcmpblnq0  7364  prarloclemcalc  7422  prarloc  7423  nqpru  7472  mullocpr  7491  distrlem4prl  7504  distrlem4pru  7505  ltprordil  7509  ltexprlemm  7520  ltexprlemopu  7523  ltexprlemupu  7524  ltexprlemru  7532  cauappcvgprlemopl  7566  cauappcvgprlem2  7580  caucvgprlemopl  7589  caucvgprlem2  7600  caucvgprprlemexbt  7626  caucvgprprlem2  7630  suplocexprlemloc  7641  suplocexprlemub  7643  suplocexprlemlub  7644  addcmpblnr  7659  mulcmpblnrlemg  7660  mulcmpblnr  7661  prsrlem1  7662  ltsrprg  7667  axmulcl  7786  ltmul1  8467  divdivdivap  8586  divmuleqap  8590  divsubdivap  8601  lt2mul2div  8750  ledivdiv  8761  lediv12a  8765  ssfzo12bi  10124  exbtwnz  10150  qbtwnre  10156  ioom  10160  seq3caopr  10382  leexp2r  10473  hashunlem  10678  recvguniq  10895  rsqrmo  10927  fsum2dlemstep  11331  expcnvre  11400  fprod2dlemstep  11519  bezout  11894  qredeu  11973  pw2dvdseu  12042  oddpwdclemdvds  12044  neiint  12545  restbasg  12568  iscnp4  12618  cnpnei  12619  cnptopco  12622  blssps  12827  blss  12828  metequiv2  12896  xmetxpbl  12908  suplociccex  13003  dedekindicc  13011  limcimolemlt  13033