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  960  imain  5300  tfrlemisucaccv  6329  tfrexlem  6338  tfr1onlemsucaccv  6345  tfrcllemsucaccv  6358  eroveu  6629  addcmpblnq  7369  mulcmpblnq  7370  ordpipqqs  7376  nqnq0pi  7440  addcmpblnq0  7445  mulcmpblnq0  7446  prarloclemcalc  7504  prarloc  7505  nqpru  7554  mullocpr  7573  distrlem4prl  7586  distrlem4pru  7587  ltprordil  7591  ltexprlemm  7602  ltexprlemopu  7605  ltexprlemupu  7606  ltexprlemru  7614  cauappcvgprlemopl  7648  cauappcvgprlem2  7662  caucvgprlemopl  7671  caucvgprlem2  7682  caucvgprprlemexbt  7708  caucvgprprlem2  7712  suplocexprlemloc  7723  suplocexprlemub  7725  suplocexprlemlub  7726  addcmpblnr  7741  mulcmpblnrlemg  7742  mulcmpblnr  7743  prsrlem1  7744  ltsrprg  7749  axmulcl  7868  ltmul1  8552  divdivdivap  8673  divmuleqap  8677  divsubdivap  8688  lt2mul2div  8839  ledivdiv  8850  lediv12a  8854  ssfzo12bi  10228  exbtwnz  10254  qbtwnre  10260  ioom  10264  seq3caopr  10486  leexp2r  10577  hashunlem  10787  recvguniq  11007  rsqrmo  11039  fsum2dlemstep  11445  expcnvre  11514  fprod2dlemstep  11633  suprzcl2dc  11959  bezout  12015  qredeu  12100  pw2dvdseu  12171  oddpwdclemdvds  12173  pcqmul  12306  pcadd  12342  pockthg  12358  grpridd  12812  issubmd  12871  unitgrp  13291  lmodprop2d  13444  lsspropdg  13523  neiint  13785  restbasg  13808  iscnp4  13858  cnpnei  13859  cnptopco  13862  blssps  14067  blss  14068  metequiv2  14136  xmetxpbl  14148  suplociccex  14243  dedekindicc  14251  limcimolemlt  14273  2sqlem5  14606