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 398

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 209  df-an 399

This theorem is referenced by:  3impdi  1346  dff13  7016  f1oiso  7107  omord2  8196  fodomacn  9485  ltapi  10328  ltmpi  10329  axpre-ltadd  10592  faclbnd  13653  pwsdiagmhm  17998  tgcl  21580  brbtwn2  26694  grpoinvf  28312  ocorth  29071  fh1  29398  fh2  29399  spansncvi  29432  lnopmi  29780  adjlnop  29866  matunitlindflem2  34893  poimirlem4  34900  heicant  34931  mblfinlem2  34934  ismblfin  34937  ftc1anclem6  34976  ftc1anclem7  34977  ftc1anc  34979