Theorem simprrl 458

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 346	. 2 |- ((ch /\ th) -> ch)
2	1	ad2antll 443	1 |- ((ph /\ (ps /\ (ch /\ th))) -> ch)

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  ordiso 5683  divdivdiv 6961  replim 8011  abl4 9413  subtopmet 10256  fbssint 10279  mdslmd1lem1 11897  axfelem16 14046  resgcom 14712  ordisoOLD 15374  alexsublem2 15438  alexsublem4 15440  reconnlem4 15449  2ndcctbss 15478  fnetr 15495  neibastop2 15523  isnrm2 15552  opnfbas 15557  ufileu 15573  rnelfmlem 15592  fmfnfmlem4 15597  fcluscf 15612  fclsfnflim 15614  flimfnfcls 15615  fcluscnplem 15617  fcluscnp 15618  filnetlem3 15642  filnetlem5 15644  ismtyhmeolem 15950  crngm4 16151  cvr1 17054  paddasslem10 17290  paddasslem12 17292  paddasslem13 17293

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-an 242

Copyright terms: Public domain