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

Theorem anandirs 829
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 824 . 2  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  ch ) )  ->  ta )
32anabsan2 820 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  3impdir  1284  oawordri  7199  omwordri  7221  oeordsuc  7243  phplem4  7699  muladd  9989  iccshftr  11654  iccshftl  11656  iccdil  11658  icccntr  11660  fzaddel  11718  fzsubel  11719  modadd1  12001  modmul1  12008  mulexp  12173  faclbnd5  12344  upxp  19887  uptx  19889  brbtwn2  23912  colinearalg  23917  eleesub  23918  eleesubd  23919  axcgrrflx  23921  axcgrid  23923  axsegconlem2  23925  phoeqi  25477  hial2eq2  25728  spansncvi  26274  5oalem3  26278  5oalem5  26280  hoscl  26368  hoeq1  26453  hoeq2  26454  hmops  26643  leopadd  26755  mdsymlem5  27030  lineintmo  29412  heicant  29654  ftc1anclem3  29697  ftc1anclem4  29698  ftc1anclem6  29700  ftc1anclem7  29701  ftc1anclem8  29702  ftc1anc  29703
  Copyright terms: Public domain W3C validator