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  5341  tfrlemisucaccv  6392  tfrexlem  6401  tfr1onlemsucaccv  6408  tfrcllemsucaccv  6421  eroveu  6694  addcmpblnq  7451  mulcmpblnq  7452  ordpipqqs  7458  nqnq0pi  7522  addcmpblnq0  7527  mulcmpblnq0  7528  prarloclemcalc  7586  prarloc  7587  nqpru  7636  mullocpr  7655  distrlem4prl  7668  distrlem4pru  7669  ltprordil  7673  ltexprlemm  7684  ltexprlemopu  7687  ltexprlemupu  7688  ltexprlemru  7696  cauappcvgprlemopl  7730  cauappcvgprlem2  7744  caucvgprlemopl  7753  caucvgprlem2  7764  caucvgprprlemexbt  7790  caucvgprprlem2  7794  suplocexprlemloc  7805  suplocexprlemub  7807  suplocexprlemlub  7808  addcmpblnr  7823  mulcmpblnrlemg  7824  mulcmpblnr  7825  prsrlem1  7826  ltsrprg  7831  axmulcl  7950  ltmul1  8636  divdivdivap  8757  divmuleqap  8761  divsubdivap  8772  lt2mul2div  8923  ledivdiv  8934  lediv12a  8938  ssfzo12bi  10318  suprzcl2dc  10346  exbtwnz  10357  qbtwnre  10363  ioom  10367  seq3caopr  10604  seqcaoprg  10605  leexp2r  10702  hashunlem  10913  recvguniq  11177  rsqrmo  11209  fsum2dlemstep  11616  expcnvre  11685  fprod2dlemstep  11804  bezout  12203  qredeu  12290  pw2dvdseu  12361  oddpwdclemdvds  12363  pcqmul  12497  pcadd  12534  pockthg  12551  grprida  13089  issubmd  13176  ghmpreima  13472  unitgrp  13748  lmodprop2d  13980  lsspropdg  14063  neiint  14465  restbasg  14488  iscnp4  14538  cnpnei  14539  cnptopco  14542  blssps  14747  blss  14748  metequiv2  14816  xmetxpbl  14828  suplociccex  14945  dedekindicc  14953  limcimolemlt  14984  lgsquad2lem2  15407  2sqlem5  15444