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

Theorem anandirs 891
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 886 . 2 (((𝜑𝜓) ∧ (𝜒𝜒)) → 𝜏)
32anabsan2 880 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 197  df-an 385
This theorem is referenced by:  3impdir  1422  oawordri  7675  omwordri  7697  oeordsuc  7719  phplem4  8183  muladd  10500  iccshftr  12344  iccshftl  12346  iccdil  12348  icccntr  12350  fzaddel  12413  fzsubel  12415  modadd1  12747  modmul1  12763  mulexp  12939  faclbnd5  13125  upxp  21474  uptx  21476  brbtwn2  25830  colinearalg  25835  eleesub  25836  eleesubd  25837  axcgrrflx  25839  axcgrid  25841  axsegconlem2  25843  phoeqi  27841  hial2eq2  28092  spansncvi  28639  5oalem3  28643  5oalem5  28645  hoscl  28732  hoeq1  28817  hoeq2  28818  hmops  29007  leopadd  29119  mdsymlem5  29394  lineintmo  32389  matunitlindflem1  33535  heicant  33574  ftc1anclem3  33617  ftc1anclem4  33618  ftc1anclem6  33620  ftc1anclem7  33621  ftc1anclem8  33622  ftc1anc  33623
  Copyright terms: Public domain W3C validator