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

Theorem anandis 869
Description: Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)
Hypothesis
Ref Expression
anandis.1 (((𝜑𝜓) ∧ (𝜑𝜒)) → 𝜏)
Assertion
Ref Expression
anandis ((𝜑 ∧ (𝜓𝜒)) → 𝜏)

Proof of Theorem anandis
StepHypRef Expression
1 anandis.1 . . 3 (((𝜑𝜓) ∧ (𝜑𝜒)) → 𝜏)
21an4s 865 . 2 (((𝜑𝜑) ∧ (𝜓𝜒)) → 𝜏)
32anabsan 850 1 ((𝜑 ∧ (𝜓𝜒)) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 196  df-an 385
This theorem is referenced by:  3impdi  1373  dff13  6394  f1oiso  6479  omord2  7512  fodomacn  8740  ltapi  9582  ltmpi  9583  axpre-ltadd  9845  faclbnd  12897  pwsdiagmhm  17141  tgcl  20532  brbtwn2  25531  grpoinvf  26564  ocorth  27328  fh1  27655  fh2  27656  spansncvi  27689  lnopmi  28037  adjlnop  28123  matunitlindflem2  32370  poimirlem4  32377  heicant  32408  mblfinlem2  32411  ismblfin  32414  ftc1anclem6  32454  ftc1anclem7  32455  ftc1anc  32457
  Copyright terms: Public domain W3C validator