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  6600  tfrexlem  6609  tfr1onlemsucaccv  6616  tfrcllemsucaccv  6629  eroveu  6904  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  10660  infssfzcldc  10686  infssfzledc  10687  suprzcl2dc  10691  exbtwnz  10702  qbtwnre  10708  ioom  10712  seq3caopr  10953  seqcaoprg  10954  leexp2r  11051  hashunlem  11266  hashfibclem  11304  wrd2ind  11517  recvguniq  11783  rsqrmo  11815  fsum2dlemstep  12226  expcnvre  12295  fprod2dlemstep  12414  bezout  12813  qredeu  12900  pwbdvdseu  12972  nnmaxpwlemdvds  12974  nnmaxpwlemparts  12977  pcqmul  13111  pcadd  13148  pockthg  13165  grprida  13766  issubmd  13840  ghmpreima  14128  gsum2d2fi  14274  unitgrp  14532  lmodprop2d  14794  lsspropdg  14877  assapropd  15123  neiint  15371  restbasg  15394  iscnp4  15444  cnpnei  15445  cnptopco  15448  blssps  15653  blss  15654  metequiv2  15722  xmetxpbl  15734  suplociccex  15851  dedekindicc  15859  limcimolemlt  15890  pellexlem3  16231  lgsquad2lem2  16406  2sqlem5  16443