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  7015  f1oiso  7106  omord2  8195  fodomacn  9484  ltapi  10327  ltmpi  10328  axpre-ltadd  10591  faclbnd  13653  pwsdiagmhm  17997  tgcl  21579  brbtwn2  26693  grpoinvf  28311  ocorth  29070  fh1  29397  fh2  29398  spansncvi  29431  lnopmi  29779  adjlnop  29865  matunitlindflem2  34891  poimirlem4  34898  heicant  34929  mblfinlem2  34932  ismblfin  34935  ftc1anclem6  34974  ftc1anclem7  34975  ftc1anc  34977