MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  anandirs 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  5772  oawordri  6729  omwordri  6751  oeordsuc  6773  phplem4  7225  muladd  9398  iccshftr  10962  iccshftl  10964  iccdil  10966  icccntr  10968  fzaddel  11019  fzsubel  11020  modadd1  11205  modmul1  11206  mulexp  11346  faclbnd5  11516  upxp  17576  uptx  17578  phoeqi  22207  hial2eq2  22457  spansncvi  23002  5oalem3  23006  5oalem5  23008  hoscl  23096  hoeq1  23181  hoeq2  23182  hmops  23371  leopadd  23483  mdsymlem5  23758  brbtwn2  25558  colinearalg  25563  eleesub  25564  eleesubd  25565  axcgrrflx  25567  axcgrid  25569  axsegconlem2  25571  lineintmo  25805
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