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  5644  oawordri  6564  omwordri  6586  oeordsuc  6608  phplem4  7059  muladd  9228  iccshftr  10785  iccshftl  10787  iccdil  10789  icccntr  10791  fzaddel  10842  fzsubel  10843  modadd1  11017  modmul1  11018  mulexp  11157  faclbnd5  11327  upxp  17333  uptx  17335  phoeqi  21452  hial2eq2  21702  spansncvi  22247  5oalem3  22251  5oalem5  22253  hoscl  22341  hoeq1  22426  hoeq2  22427  hmops  22616  leopadd  22728  mdsymlem5  23003  brbtwn2  24605  colinearalg  24610  eleesub  24611  eleesubd  24612  axcgrrflx  24614  axcgrid  24616  axsegconlem2  24618  lineintmo  24852
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