Theorem simprrl 541

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  969  imain  5419  tfrlemisucaccv  6534  tfrexlem  6543  tfr1onlemsucaccv  6550  tfrcllemsucaccv  6563  eroveu  6838  addcmpblnq  7630  mulcmpblnq  7631  ordpipqqs  7637  nqnq0pi  7701  addcmpblnq0  7706  mulcmpblnq0  7707  prarloclemcalc  7765  prarloc  7766  nqpru  7815  mullocpr  7834  distrlem4prl  7847  distrlem4pru  7848  ltprordil  7852  ltexprlemm  7863  ltexprlemopu  7866  ltexprlemupu  7867  ltexprlemru  7875  cauappcvgprlemopl  7909  cauappcvgprlem2  7923  caucvgprlemopl  7932  caucvgprlem2  7943  caucvgprprlemexbt  7969  caucvgprprlem2  7973  suplocexprlemloc  7984  suplocexprlemub  7986  suplocexprlemlub  7987  addcmpblnr  8002  mulcmpblnrlemg  8003  mulcmpblnr  8004  prsrlem1  8005  ltsrprg  8010  axmulcl  8129  ltmul1  8815  divdivdivap  8936  divmuleqap  8940  divsubdivap  8951  lt2mul2div  9102  ledivdiv  9113  lediv12a  9117  ssfzo12bi  10514  suprzcl2dc  10543  exbtwnz  10554  qbtwnre  10560  ioom  10564  seq3caopr  10801  seqcaoprg  10802  leexp2r  10899  hashunlem  11111  wrd2ind  11351  recvguniq  11616  rsqrmo  11648  fsum2dlemstep  12056  expcnvre  12125  fprod2dlemstep  12244  bezout  12643  qredeu  12730  pw2dvdseu  12801  oddpwdclemdvds  12803  pcqmul  12937  pcadd  12974  pockthg  12991  grprida  13531  issubmd  13618  ghmpreima  13914  unitgrp  14192  lmodprop2d  14424  lsspropdg  14507  neiint  14936  restbasg  14959  iscnp4  15009  cnpnei  15010  cnptopco  15013  blssps  15218  blss  15219  metequiv2  15287  xmetxpbl  15299  suplociccex  15416  dedekindicc  15424  limcimolemlt  15455  pellexlem3  15773  lgsquad2lem2  15881  2sqlem5  15918