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

Theorem anandirs 675
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 656 . 2 (((𝜑𝜓) ∧ (𝜒𝜒)) → 𝜏)
32anabsan2 670 1 (((𝜑𝜓) ∧ 𝜒) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  3impdir  1345  oawordri  8169  omwordri  8191  oeordsuc  8213  phplem4  8691  muladd  11064  iccshftr  12865  iccshftl  12867  iccdil  12869  icccntr  12871  fzaddel  12934  fzsubel  12936  modadd1  13269  modmul1  13285  mulexp  13461  faclbnd5  13651  upxp  22147  uptx  22149  brbtwn2  26605  colinearalg  26610  eleesub  26611  eleesubd  26612  axcgrrflx  26614  axcgrid  26616  axsegconlem2  26618  phoeqi  28548  hial2eq2  28798  spansncvi  29343  5oalem3  29347  5oalem5  29349  hoscl  29436  hoeq1  29521  hoeq2  29522  hmops  29711  leopadd  29823  mdsymlem5  30098  lineintmo  33502  matunitlindflem1  34755  heicant  34794  ftc1anclem3  34836  ftc1anclem4  34837  ftc1anclem6  34839  ftc1anclem7  34840  ftc1anclem8  34841  ftc1anc  34842
  Copyright terms: Public domain W3C validator