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

Theorem anandirs 806
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 801 . 2  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  ch ) )  ->  ta )
32anabsan2 797 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  3impdir  1241  fvreseq  5835  oawordri  6795  omwordri  6817  oeordsuc  6839  phplem4  7291  muladd  9468  iccshftr  11032  iccshftl  11034  iccdil  11036  icccntr  11038  fzaddel  11089  fzsubel  11090  modadd1  11280  modmul1  11281  mulexp  11421  faclbnd5  11591  upxp  17657  uptx  17659  phoeqi  22361  hial2eq2  22611  spansncvi  23156  5oalem3  23160  5oalem5  23162  hoscl  23250  hoeq1  23335  hoeq2  23336  hmops  23525  leopadd  23637  mdsymlem5  23912  brbtwn2  25846  colinearalg  25851  eleesub  25852  eleesubd  25853  axcgrrflx  25855  axcgrid  25857  axsegconlem2  25859  lineintmo  26093  ftc1anclem3  26284  ftc1anclem4  26285  ftc1anclem6  26287  ftc1anclem7  26288  ftc1anclem8  26289  ftc1anc  26290
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator