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

Theorem anandirs 827
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 822 . 2  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  ch ) )  ->  ta )
32anabsan2 818 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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
This theorem is referenced by:  3impdir  1274  oawordri  6988  omwordri  7010  oeordsuc  7032  phplem4  7492  muladd  9776  iccshftr  11418  iccshftl  11420  iccdil  11422  icccntr  11424  fzaddel  11492  fzsubel  11493  modadd1  11744  modmul1  11751  mulexp  11902  faclbnd5  12073  upxp  19195  uptx  19197  brbtwn2  23150  colinearalg  23155  eleesub  23156  eleesubd  23157  axcgrrflx  23159  axcgrid  23161  axsegconlem2  23163  phoeqi  24257  hial2eq2  24508  spansncvi  25054  5oalem3  25058  5oalem5  25060  hoscl  25148  hoeq1  25233  hoeq2  25234  hmops  25423  leopadd  25535  mdsymlem5  25810  lineintmo  28187  heicant  28424  ftc1anclem3  28467  ftc1anclem4  28468  ftc1anclem6  28470  ftc1anclem7  28471  ftc1anclem8  28472  ftc1anc  28473
  Copyright terms: Public domain W3C validator