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

Step	Hyp	Ref	Expression
1		anandis.1	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)) → 𝜏)
2	1	an4s 865	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) → 𝜏)
3	2	anabsan 850	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜏)

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  6416  f1oiso  6501  omord2  7534  fodomacn  8762  ltapi  9604  ltmpi  9605  axpre-ltadd  9867  faclbnd  12939  pwsdiagmhm  17192  tgcl  20584  brbtwn2  25585  grpoinvf  26770  ocorth  27534  fh1  27861  fh2  27862  spansncvi  27895  lnopmi  28243  adjlnop  28329  matunitlindflem2  32576  poimirlem4  32583  heicant  32614  mblfinlem2  32617  ismblfin  32620  ftc1anclem6  32660  ftc1anclem7  32661  ftc1anc  32663