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

Theorem anandirs 804
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 799 . 2  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  ch ) )  ->  ta )
32anabsan2 795 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  3impdir  1238  fvreseq  5630  oawordri  6550  omwordri  6572  oeordsuc  6594  phplem4  7045  muladd  9214  iccshftr  10771  iccshftl  10773  iccdil  10775  icccntr  10777  fzaddel  10828  fzsubel  10829  modadd1  11003  modmul1  11004  mulexp  11143  faclbnd5  11313  upxp  17319  uptx  17321  phoeqi  21438  hial2eq2  21688  spansncvi  22233  5oalem3  22237  5oalem5  22239  hoscl  22327  hoeq1  22412  hoeq2  22413  hmops  22602  leopadd  22714  mdsymlem5  22989  brbtwn2  24535  colinearalg  24540  eleesub  24541  eleesubd  24542  axcgrrflx  24544  axcgrid  24546  axsegconlem2  24548  lineintmo  24782
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 177  df-an 360
  Copyright terms: Public domain W3C validator