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  5628  oawordri  6548  omwordri  6570  oeordsuc  6592  phplem4  7043  muladd  9212  iccshftr  10769  iccshftl  10771  iccdil  10773  icccntr  10775  fzaddel  10826  fzsubel  10827  modadd1  11001  modmul1  11002  mulexp  11141  faclbnd5  11311  upxp  17317  uptx  17319  phoeqi  21436  hial2eq2  21686  spansncvi  22231  5oalem3  22235  5oalem5  22237  hoscl  22325  hoeq1  22410  hoeq2  22411  hmops  22600  leopadd  22712  mdsymlem5  22987  brbtwn2  24533  colinearalg  24538  eleesub  24539  eleesubd  24540  axcgrrflx  24542  axcgrid  24544  axsegconlem2  24546  lineintmo  24780
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