Theorem anabsi5 817

Description: Absorption of antecedent into conjunction. (Contributed by NM, 11-Jun-1995.) (Proof shortened by Wolf Lammen, 18-Nov-2013.)

Hypothesis

Ref	Expression
anabsi5.1

Assertion

Ref	Expression
anabsi5

Proof of Theorem anabsi5

Step	Hyp	Ref	Expression
1		anabsi5.1	. . 3
2	1	imp 429	. 2
3	2	anabss5 816	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  anabsi6  818  anabsi8  820  3anidm12  1285  rspce  3205  onint  6630  f1oweALT  6784  php2  7722  hasheqf1oi  12424  ptcmpfi  20314  redwlk  24608  vdusgraval  24907  relexpsucl  29055  relexpcnv  29056  relexpdm  29058  relexprn  29059  rtrclreclem.trans  29069  rtrclreclem.min  29070  diophin  30706  diophun  30707  rspcegf  31398  stoweidlem36  31818

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

This theorem depends on definitions:  df-bi 185  df-an 371