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

Theorem anandirs 805
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 800 . 2  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  ch ) )  ->  ta )
32anabsan2 796 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  3impdir  1240  fvreseq  5825  oawordri  6785  omwordri  6807  oeordsuc  6829  phplem4  7281  muladd  9458  iccshftr  11022  iccshftl  11024  iccdil  11026  icccntr  11028  fzaddel  11079  fzsubel  11080  modadd1  11270  modmul1  11271  mulexp  11411  faclbnd5  11581  upxp  17647  uptx  17649  phoeqi  22351  hial2eq2  22601  spansncvi  23146  5oalem3  23150  5oalem5  23152  hoscl  23240  hoeq1  23325  hoeq2  23326  hmops  23515  leopadd  23627  mdsymlem5  23902  brbtwn2  25836  colinearalg  25841  eleesub  25842  eleesubd  25843  axcgrrflx  25845  axcgrid  25847  axsegconlem2  25849  lineintmo  26083  ftc1anclem3  26272  ftc1anclem4  26273  ftc1anclem6  26275  ftc1anclem7  26276  ftc1anclem8  26277  ftc1anc  26278
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 178  df-an 361
  Copyright terms: Public domain W3C validator