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

Theorem anandis 677
 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 659 . 2 (((𝜑𝜑) ∧ (𝜓𝜒)) → 𝜏)
32anabsan 664 1 ((𝜑 ∧ (𝜓𝜒)) → 𝜏)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  3impdi  1347  dff13  7005  f1oiso  7098  omord2  8203  fodomacn  9516  ltapi  10363  ltmpi  10364  axpre-ltadd  10627  faclbnd  13700  pwsdiagmhm  18061  tgcl  21669  brbtwn2  26798  grpoinvf  28414  ocorth  29173  fh1  29500  fh2  29501  spansncvi  29534  lnopmi  29882  adjlnop  29968  matunitlindflem2  35334  poimirlem4  35341  heicant  35372  mblfinlem2  35375  ismblfin  35378  ftc1anclem6  35415  ftc1anclem7  35416  ftc1anc  35418
 Copyright terms: Public domain W3C validator