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

Theorem anandirs 829
Description: Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)
Hypothesis
Ref Expression
anandirs.1  |-  ( ( ( ph  /\  ch )  /\  ( ps  /\  ch ) )  ->  ta )
Assertion
Ref Expression
anandirs  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ta )

Proof of Theorem anandirs
StepHypRef Expression
1 anandirs.1 . . 3  |-  ( ( ( ph  /\  ch )  /\  ( ps  /\  ch ) )  ->  ta )
21an4s 824 . 2  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  ch ) )  ->  ta )
32anabsan2 820 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  3impdir  1282  oawordri  7117  omwordri  7139  oeordsuc  7161  phplem4  7618  muladd  9907  iccshftr  11575  iccshftl  11577  iccdil  11579  icccntr  11581  fzaddel  11640  fzsubel  11641  modadd1  11934  modmul1  11943  mulexp  12108  faclbnd5  12278  upxp  20209  uptx  20211  brbtwn2  24329  colinearalg  24334  eleesub  24335  eleesubd  24336  axcgrrflx  24338  axcgrid  24340  axsegconlem2  24342  phoeqi  25890  hial2eq2  26141  spansncvi  26687  5oalem3  26691  5oalem5  26693  hoscl  26780  hoeq1  26865  hoeq2  26866  hmops  27055  leopadd  27167  mdsymlem5  27442  lineintmo  29960  heicant  30214  ftc1anclem3  30258  ftc1anclem4  30259  ftc1anclem6  30261  ftc1anclem7  30262  ftc1anclem8  30263  ftc1anc  30264
  Copyright terms: Public domain W3C validator