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

Theorem anandirs 869
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 864 . 2 (((𝜑𝜓) ∧ (𝜒𝜒)) → 𝜏)
32anabsan2 858 1 (((𝜑𝜓) ∧ 𝜒) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  3impdir  1373  oawordri  7494  omwordri  7516  oeordsuc  7538  phplem4  8004  muladd  10313  iccshftr  12135  iccshftl  12137  iccdil  12139  icccntr  12141  fzaddel  12203  fzsubel  12205  modadd1  12526  modmul1  12542  mulexp  12718  faclbnd5  12904  upxp  21183  uptx  21185  brbtwn2  25530  colinearalg  25535  eleesub  25536  eleesubd  25537  axcgrrflx  25539  axcgrid  25541  axsegconlem2  25543  phoeqi  26890  hial2eq2  27141  spansncvi  27688  5oalem3  27692  5oalem5  27694  hoscl  27781  hoeq1  27866  hoeq2  27867  hmops  28056  leopadd  28168  mdsymlem5  28443  lineintmo  31227  matunitlindflem1  32358  heicant  32397  ftc1anclem3  32440  ftc1anclem4  32441  ftc1anclem6  32443  ftc1anclem7  32444  ftc1anclem8  32445  ftc1anc  32446
  Copyright terms: Public domain W3C validator