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  7734  mulcmpblnq  7735  ordpipqqs  7741  nqnq0pi  7805  addcmpblnq0  7810  mulcmpblnq0  7811  prarloclemcalc  7869  prarloc  7870  nqpru  7919  mullocpr  7938  distrlem4prl  7951  distrlem4pru  7952  ltprordil  7956  ltexprlemm  7967  ltexprlemopu  7970  ltexprlemupu  7971  ltexprlemru  7979  cauappcvgprlemopl  8013  cauappcvgprlem2  8027  caucvgprlemopl  8036  caucvgprlem2  8047  caucvgprprlemexbt  8073  caucvgprprlem2  8077  suplocexprlemloc  8088  suplocexprlemub  8090  suplocexprlemlub  8091  addcmpblnr  8106  mulcmpblnrlemg  8107  mulcmpblnr  8108  prsrlem1  8109  ltsrprg  8114  axmulcl  8233  ltmul1  8922  divdivdivap  9045  divmuleqap  9049  divsubdivap  9060  lt2mul2div  9211  ledivdiv  9222  lediv12a  9226  ssfzo12bi  10653  infssfzcldc  10679  infssfzledc  10680  suprzcl2dc  10684  exbtwnz  10695  qbtwnre  10701  ioom  10705  seq3caopr  10945  seqcaoprg  10946  leexp2r  11043  hashunlem  11258  hashfibclem  11296  wrd2ind  11509  recvguniq  11775  rsqrmo  11807  fsum2dlemstep  12217  expcnvre  12286  fprod2dlemstep  12405  bezout  12804  qredeu  12891  pwbdvdseu  12963  nnmaxpwlemdvds  12965  nnmaxpwlemparts  12968  pcqmul  13102  pcadd  13139  pockthg  13156  grprida  13756  issubmd  13830  ghmpreima  14118  unitgrp  14472  lmodprop2d  14734  lsspropdg  14817  assapropd  15063  neiint  15295  restbasg  15318  iscnp4  15368  cnpnei  15369  cnptopco  15372  blssps  15577  blss  15578  metequiv2  15646  xmetxpbl  15658  suplociccex  15775  dedekindicc  15783  limcimolemlt  15814  pellexlem3  16150  lgsquad2lem2  16299  2sqlem5  16336