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

Theorem anandirs 870
Description: Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)
Hypothesis
Ref Expression
anandirs.1 (((𝜑𝜒) ∧ (𝜓𝜒)) → 𝜏)
Assertion
Ref Expression
anandirs (((𝜑𝜓) ∧ 𝜒) → 𝜏)

Proof of Theorem anandirs
StepHypRef Expression
1 anandirs.1 . . 3 (((𝜑𝜒) ∧ (𝜓𝜒)) → 𝜏)
21an4s 865 . 2 (((𝜑𝜓) ∧ (𝜒𝜒)) → 𝜏)
32anabsan2 859 1 (((𝜑𝜓) ∧ 𝜒) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 196  df-an 385
This theorem is referenced by:  3impdir  1374  oawordri  7517  omwordri  7539  oeordsuc  7561  phplem4  8027  muladd  10341  iccshftr  12177  iccshftl  12179  iccdil  12181  icccntr  12183  fzaddel  12246  fzsubel  12248  modadd1  12569  modmul1  12585  mulexp  12761  faclbnd5  12947  upxp  21236  uptx  21238  brbtwn2  25585  colinearalg  25590  eleesub  25591  eleesubd  25592  axcgrrflx  25594  axcgrid  25596  axsegconlem2  25598  phoeqi  27097  hial2eq2  27348  spansncvi  27895  5oalem3  27899  5oalem5  27901  hoscl  27988  hoeq1  28073  hoeq2  28074  hmops  28263  leopadd  28375  mdsymlem5  28650  lineintmo  31434  matunitlindflem1  32575  heicant  32614  ftc1anclem3  32657  ftc1anclem4  32658  ftc1anclem6  32660  ftc1anclem7  32661  ftc1anclem8  32662  ftc1anc  32663
  Copyright terms: Public domain W3C validator