Theorem anandis 676

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 658	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) → 𝜏)
3	2	anabsan 663	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  3impdi  1350  dff13  7160  f1oiso  7254  omord2  8429  fodomacn  9858  ltapi  10705  ltmpi  10706  axpre-ltadd  10969  faclbnd  14050  pwsdiagmhm  18514  tgcl  22164  brbtwn2  27318  grpoinvf  28939  ocorth  29698  fh1  30025  fh2  30026  spansncvi  30059  lnopmi  30407  adjlnop  30493  matunitlindflem2  35818  poimirlem4  35825  heicant  35856  mblfinlem2  35859  ismblfin  35862  ftc1anclem6  35899  ftc1anclem7  35900  ftc1anc  35902