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  966  imain  5402  tfrlemisucaccv  6469  tfrexlem  6478  tfr1onlemsucaccv  6485  tfrcllemsucaccv  6498  eroveu  6771  addcmpblnq  7550  mulcmpblnq  7551  ordpipqqs  7557  nqnq0pi  7621  addcmpblnq0  7626  mulcmpblnq0  7627  prarloclemcalc  7685  prarloc  7686  nqpru  7735  mullocpr  7754  distrlem4prl  7767  distrlem4pru  7768  ltprordil  7772  ltexprlemm  7783  ltexprlemopu  7786  ltexprlemupu  7787  ltexprlemru  7795  cauappcvgprlemopl  7829  cauappcvgprlem2  7843  caucvgprlemopl  7852  caucvgprlem2  7863  caucvgprprlemexbt  7889  caucvgprprlem2  7893  suplocexprlemloc  7904  suplocexprlemub  7906  suplocexprlemlub  7907  addcmpblnr  7922  mulcmpblnrlemg  7923  mulcmpblnr  7924  prsrlem1  7925  ltsrprg  7930  axmulcl  8049  ltmul1  8735  divdivdivap  8856  divmuleqap  8860  divsubdivap  8871  lt2mul2div  9022  ledivdiv  9033  lediv12a  9037  ssfzo12bi  10426  suprzcl2dc  10454  exbtwnz  10465  qbtwnre  10471  ioom  10475  seq3caopr  10712  seqcaoprg  10713  leexp2r  10810  hashunlem  11021  wrd2ind  11250  recvguniq  11501  rsqrmo  11533  fsum2dlemstep  11940  expcnvre  12009  fprod2dlemstep  12128  bezout  12527  qredeu  12614  pw2dvdseu  12685  oddpwdclemdvds  12687  pcqmul  12821  pcadd  12858  pockthg  12875  grprida  13415  issubmd  13502  ghmpreima  13798  unitgrp  14074  lmodprop2d  14306  lsspropdg  14389  neiint  14813  restbasg  14836  iscnp4  14886  cnpnei  14887  cnptopco  14890  blssps  15095  blss  15096  metequiv2  15164  xmetxpbl  15176  suplociccex  15293  dedekindicc  15301  limcimolemlt  15332  lgsquad2lem2  15755  2sqlem5  15792