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

Theorem anandirs 661
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 642 . 2 (((𝜑𝜓) ∧ (𝜒𝜒)) → 𝜏)
32anabsan2 656 1 (((𝜑𝜓) ∧ 𝜒) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 198  df-an 385
This theorem is referenced by:  3impdir  1453  oawordri  7876  omwordri  7898  oeordsuc  7920  phplem4  8390  muladd  10756  iccshftr  12548  iccshftl  12550  iccdil  12552  icccntr  12554  fzaddel  12617  fzsubel  12619  modadd1  12950  modmul1  12966  mulexp  13141  faclbnd5  13324  upxp  21660  uptx  21662  brbtwn2  26021  colinearalg  26026  eleesub  26027  eleesubd  26028  axcgrrflx  26030  axcgrid  26032  axsegconlem2  26034  phoeqi  28063  hial2eq2  28314  spansncvi  28861  5oalem3  28865  5oalem5  28867  hoscl  28954  hoeq1  29039  hoeq2  29040  hmops  29229  leopadd  29341  mdsymlem5  29616  lineintmo  32606  matunitlindflem1  33736  heicant  33775  ftc1anclem3  33817  ftc1anclem4  33818  ftc1anclem6  33820  ftc1anclem7  33821  ftc1anclem8  33822  ftc1anc  33823
  Copyright terms: Public domain W3C validator