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  5463  tfrlemisucaccv  6596  tfrexlem  6605  tfr1onlemsucaccv  6612  tfrcllemsucaccv  6625  eroveu  6900  addcmpblnq  7735  mulcmpblnq  7736  ordpipqqs  7742  nqnq0pi  7806  addcmpblnq0  7811  mulcmpblnq0  7812  prarloclemcalc  7870  prarloc  7871  nqpru  7920  mullocpr  7939  distrlem4prl  7952  distrlem4pru  7953  ltprordil  7957  ltexprlemm  7968  ltexprlemopu  7971  ltexprlemupu  7972  ltexprlemru  7980  cauappcvgprlemopl  8014  cauappcvgprlem2  8028  caucvgprlemopl  8037  caucvgprlem2  8048  caucvgprprlemexbt  8074  caucvgprprlem2  8078  suplocexprlemloc  8089  suplocexprlemub  8091  suplocexprlemlub  8092  addcmpblnr  8107  mulcmpblnrlemg  8108  mulcmpblnr  8109  prsrlem1  8110  ltsrprg  8115  axmulcl  8234  ltmul1  8923  divdivdivap  9046  divmuleqap  9050  divsubdivap  9061  lt2mul2div  9212  ledivdiv  9223  lediv12a  9227  ssfzo12bi  10654  infssfzcldc  10680  infssfzledc  10681  suprzcl2dc  10685  exbtwnz  10696  qbtwnre  10702  ioom  10706  seq3caopr  10947  seqcaoprg  10948  leexp2r  11045  hashunlem  11260  hashfibclem  11298  wrd2ind  11511  recvguniq  11777  rsqrmo  11809  fsum2dlemstep  12220  expcnvre  12289  fprod2dlemstep  12408  bezout  12807  qredeu  12894  pwbdvdseu  12966  nnmaxpwlemdvds  12968  nnmaxpwlemparts  12971  pcqmul  13105  pcadd  13142  pockthg  13159  grprida  13760  issubmd  13834  ghmpreima  14122  unitgrp  14507  lmodprop2d  14769  lsspropdg  14852  assapropd  15098  neiint  15337  restbasg  15360  iscnp4  15410  cnpnei  15411  cnptopco  15414  blssps  15619  blss  15620  metequiv2  15688  xmetxpbl  15700  suplociccex  15817  dedekindicc  15825  limcimolemlt  15856  pellexlem3  16192  lgsquad2lem2  16367  2sqlem5  16404