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

Theorem anandirs 678
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 659 . 2 (((𝜑𝜓) ∧ (𝜒𝜒)) → 𝜏)
32anabsan2 673 1 (((𝜑𝜓) ∧ 𝜒) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  3impdir  1352  oawordri  8546  omwordri  8568  oeordsuc  8590  phplem2  9204  phplem4OLD  9216  muladd  11642  iccshftr  13459  iccshftl  13461  iccdil  13463  icccntr  13465  fzaddel  13531  fzsubel  13533  modadd1  13869  modmul1  13885  mulexp  14063  faclbnd5  14254  upxp  23109  uptx  23111  brbtwn2  28143  colinearalg  28148  eleesub  28149  eleesubd  28150  axcgrrflx  28152  axcgrid  28154  axsegconlem2  28156  phoeqi  30088  hial2eq2  30338  spansncvi  30883  5oalem3  30887  5oalem5  30889  hoscl  30976  hoeq1  31061  hoeq2  31062  hmops  31251  leopadd  31363  mdsymlem5  31638  lineintmo  35067  matunitlindflem1  36422  heicant  36461  ftc1anclem3  36501  ftc1anclem4  36502  ftc1anclem6  36504  ftc1anclem7  36505  ftc1anclem8  36506  ftc1anc  36507
  Copyright terms: Public domain W3C validator