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

Theorem anandirs 831
Description: Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)
Hypothesis
Ref Expression
anandirs.1
Assertion
Ref Expression
anandirs

Proof of Theorem anandirs
StepHypRef Expression
1 anandirs.1 . . 3
21an4s 826 . 2
32anabsan2 822 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  3impdir  1284  oawordri  7218  omwordri  7240  oeordsuc  7262  phplem4  7719  muladd  10014  iccshftr  11683  iccshftl  11685  iccdil  11687  icccntr  11689  fzaddel  11747  fzsubel  11748  modadd1  12033  modmul1  12040  mulexp  12205  faclbnd5  12376  upxp  20124  uptx  20126  brbtwn2  24208  colinearalg  24213  eleesub  24214  eleesubd  24215  axcgrrflx  24217  axcgrid  24219  axsegconlem2  24221  phoeqi  25773  hial2eq2  26024  spansncvi  26570  5oalem3  26574  5oalem5  26576  hoscl  26664  hoeq1  26749  hoeq2  26750  hmops  26939  leopadd  27051  mdsymlem5  27326  lineintmo  29807  heicant  30049  ftc1anclem3  30092  ftc1anclem4  30093  ftc1anclem6  30095  ftc1anclem7  30096  ftc1anclem8  30097  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