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

Theorem anandirs 679
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 660 . 2 (((𝜑𝜓) ∧ (𝜒𝜒)) → 𝜏)
32anabsan2 674 1 (((𝜑𝜓) ∧ 𝜒) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  3impdir  1352  oawordri  8588  omwordri  8610  oeordsuc  8632  phplem2  9245  phplem4OLD  9257  muladd  11695  iccshftr  13526  iccshftl  13528  iccdil  13530  icccntr  13532  fzaddel  13598  fzsubel  13600  modadd1  13948  modmul1  13965  mulexp  14142  faclbnd5  14337  upxp  23631  uptx  23633  brbtwn2  28920  colinearalg  28925  eleesub  28926  eleesubd  28927  axcgrrflx  28929  axcgrid  28931  axsegconlem2  28933  phoeqi  30876  hial2eq2  31126  spansncvi  31671  5oalem3  31675  5oalem5  31677  hoscl  31764  hoeq1  31849  hoeq2  31850  hmops  32039  leopadd  32151  mdsymlem5  32426  lineintmo  36158  matunitlindflem1  37623  heicant  37662  ftc1anclem3  37702  ftc1anclem4  37703  ftc1anclem6  37705  ftc1anclem7  37706  ftc1anclem8  37707  ftc1anc  37708
  Copyright terms: Public domain W3C validator