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

Theorem anandis 890
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 886 . 2 (((𝜑𝜑) ∧ (𝜓𝜒)) → 𝜏)
32anabsan 871 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 197  df-an 385
This theorem is referenced by:  3impdi  1421  dff13  6552  f1oiso  6641  omord2  7692  fodomacn  8917  ltapi  9763  ltmpi  9764  axpre-ltadd  10026  faclbnd  13117  pwsdiagmhm  17416  tgcl  20821  brbtwn2  25830  grpoinvf  27514  ocorth  28278  fh1  28605  fh2  28606  spansncvi  28639  lnopmi  28987  adjlnop  29073  matunitlindflem2  33536  poimirlem4  33543  heicant  33574  mblfinlem2  33577  ismblfin  33580  ftc1anclem6  33620  ftc1anclem7  33621  ftc1anc  33623
  Copyright terms: Public domain W3C validator