Theorem simprrl 545

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 495	1 |- ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) -> ch )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  dn1dc  973  imain  5466  tfrlemisucaccv  6601  tfrexlem  6610  tfr1onlemsucaccv  6617  tfrcllemsucaccv  6630  eroveu  6905  addcmpblnq  7740  mulcmpblnq  7741  ordpipqqs  7747  nqnq0pi  7811  addcmpblnq0  7816  mulcmpblnq0  7817  prarloclemcalc  7875  prarloc  7876  nqpru  7925  mullocpr  7944  distrlem4prl  7957  distrlem4pru  7958  ltprordil  7962  ltexprlemm  7973  ltexprlemopu  7976  ltexprlemupu  7977  ltexprlemru  7985  cauappcvgprlemopl  8019  cauappcvgprlem2  8033  caucvgprlemopl  8042  caucvgprlem2  8053  caucvgprprlemexbt  8079  caucvgprprlem2  8083  suplocexprlemloc  8094  suplocexprlemub  8096  suplocexprlemlub  8097  addcmpblnr  8112  mulcmpblnrlemg  8113  mulcmpblnr  8114  prsrlem1  8115  ltsrprg  8120  axmulcl  8239  ltmul1  8928  divdivdivap  9051  divmuleqap  9055  divsubdivap  9066  lt2mul2div  9217  ledivdiv  9228  lediv12a  9232  ssfzo12bi  10659  infssfzcldc  10685  infssfzledc  10686  suprzcl2dc  10690  exbtwnz  10701  qbtwnre  10707  ioom  10711  seq3caopr  10952  seqcaoprg  10953  leexp2r  11050  hashunlem  11265  hashfibclem  11303  wrd2ind  11516  recvguniq  11782  rsqrmo  11814  fsum2dlemstep  12225  expcnvre  12294  fprod2dlemstep  12413  bezout  12812  qredeu  12899  pwbdvdseu  12971  nnmaxpwlemdvds  12973  nnmaxpwlemparts  12976  pcqmul  13110  pcadd  13147  pockthg  13164  grprida  13765  issubmd  13839  ghmpreima  14127  gsum2d2fi  14273  unitgrp  14531  lmodprop2d  14793  lsspropdg  14876  assapropd  15122  mplsubgfilemcl  15232  neiint  15388  restbasg  15411  iscnp4  15461  cnpnei  15462  cnptopco  15465  blssps  15670  blss  15671  metequiv2  15739  xmetxpbl  15751  suplociccex  15868  dedekindicc  15876  limcimolemlt  15907  pellexlem3  16248  lgsquad2lem2  16423  2sqlem5  16460