MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  anandis Unicode version

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
StepHypRef Expression
1 anandis.1 . . 3
21an4s 826 . 2
32anabsan 813 1
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator