Theorem simprrl 539

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

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:  dn1dc  962  imain  5340  tfrlemisucaccv  6383  tfrexlem  6392  tfr1onlemsucaccv  6399  tfrcllemsucaccv  6412  eroveu  6685  addcmpblnq  7434  mulcmpblnq  7435  ordpipqqs  7441  nqnq0pi  7505  addcmpblnq0  7510  mulcmpblnq0  7511  prarloclemcalc  7569  prarloc  7570  nqpru  7619  mullocpr  7638  distrlem4prl  7651  distrlem4pru  7652  ltprordil  7656  ltexprlemm  7667  ltexprlemopu  7670  ltexprlemupu  7671  ltexprlemru  7679  cauappcvgprlemopl  7713  cauappcvgprlem2  7727  caucvgprlemopl  7736  caucvgprlem2  7747  caucvgprprlemexbt  7773  caucvgprprlem2  7777  suplocexprlemloc  7788  suplocexprlemub  7790  suplocexprlemlub  7791  addcmpblnr  7806  mulcmpblnrlemg  7807  mulcmpblnr  7808  prsrlem1  7809  ltsrprg  7814  axmulcl  7933  ltmul1  8619  divdivdivap  8740  divmuleqap  8744  divsubdivap  8755  lt2mul2div  8906  ledivdiv  8917  lediv12a  8921  ssfzo12bi  10301  suprzcl2dc  10329  exbtwnz  10340  qbtwnre  10346  ioom  10350  seq3caopr  10587  seqcaoprg  10588  leexp2r  10685  hashunlem  10896  recvguniq  11160  rsqrmo  11192  fsum2dlemstep  11599  expcnvre  11668  fprod2dlemstep  11787  bezout  12178  qredeu  12265  pw2dvdseu  12336  oddpwdclemdvds  12338  pcqmul  12472  pcadd  12509  pockthg  12526  grprida  13030  issubmd  13106  ghmpreima  13396  unitgrp  13672  lmodprop2d  13904  lsspropdg  13987  neiint  14381  restbasg  14404  iscnp4  14454  cnpnei  14455  cnptopco  14458  blssps  14663  blss  14664  metequiv2  14732  xmetxpbl  14744  suplociccex  14861  dedekindicc  14869  limcimolemlt  14900  lgsquad2lem2  15323  2sqlem5  15360