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  5409  tfrlemisucaccv  6486  tfrexlem  6495  tfr1onlemsucaccv  6502  tfrcllemsucaccv  6515  eroveu  6790  addcmpblnq  7577  mulcmpblnq  7578  ordpipqqs  7584  nqnq0pi  7648  addcmpblnq0  7653  mulcmpblnq0  7654  prarloclemcalc  7712  prarloc  7713  nqpru  7762  mullocpr  7781  distrlem4prl  7794  distrlem4pru  7795  ltprordil  7799  ltexprlemm  7810  ltexprlemopu  7813  ltexprlemupu  7814  ltexprlemru  7822  cauappcvgprlemopl  7856  cauappcvgprlem2  7870  caucvgprlemopl  7879  caucvgprlem2  7890  caucvgprprlemexbt  7916  caucvgprprlem2  7920  suplocexprlemloc  7931  suplocexprlemub  7933  suplocexprlemlub  7934  addcmpblnr  7949  mulcmpblnrlemg  7950  mulcmpblnr  7951  prsrlem1  7952  ltsrprg  7957  axmulcl  8076  ltmul1  8762  divdivdivap  8883  divmuleqap  8887  divsubdivap  8898  lt2mul2div  9049  ledivdiv  9060  lediv12a  9064  ssfzo12bi  10460  suprzcl2dc  10489  exbtwnz  10500  qbtwnre  10506  ioom  10510  seq3caopr  10747  seqcaoprg  10748  leexp2r  10845  hashunlem  11057  wrd2ind  11294  recvguniq  11546  rsqrmo  11578  fsum2dlemstep  11985  expcnvre  12054  fprod2dlemstep  12173  bezout  12572  qredeu  12659  pw2dvdseu  12730  oddpwdclemdvds  12732  pcqmul  12866  pcadd  12903  pockthg  12920  grprida  13460  issubmd  13547  ghmpreima  13843  unitgrp  14120  lmodprop2d  14352  lsspropdg  14435  neiint  14859  restbasg  14882  iscnp4  14932  cnpnei  14933  cnptopco  14936  blssps  15141  blss  15142  metequiv2  15210  xmetxpbl  15222  suplociccex  15339  dedekindicc  15347  limcimolemlt  15378  lgsquad2lem2  15801  2sqlem5  15838