Theorem anandis 830

Description: Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)

Hypothesis

Ref	Expression
anandis.1

Assertion

Ref	Expression
anandis

Proof of Theorem anandis

Step	Hyp	Ref	Expression
1		anandis.1	. . 3
2	1	an4s 826	. 2
3	2	anabsan 813	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  3impdi  1283  dff13  6166  f1oiso  6247  omord2  7235  fodomacn  8458  ltapi  9302  ltmpi  9303  axpre-ltadd  9565  faclbnd  12368  pwsdiagmhm  16000  tgcl  19471  brbtwn2  24208  grpoinvf  25242  ocorth  26209  fh1  26536  fh2  26537  spansncvi  26570  lnopmi  26919  adjlnop  27005  heicant  30049  mblfinlem2  30052  ismblfin  30055  ftc1anclem6  30095  ftc1anclem7  30096  ftc1anc  30098

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