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  6394  f1oiso  6479  omord2  7512  fodomacn  8740  ltapi  9582  ltmpi  9583  axpre-ltadd  9845  faclbnd  12897  pwsdiagmhm  17141  tgcl  20532  brbtwn2  25531  grpoinvf  26564  ocorth  27328  fh1  27655  fh2  27656  spansncvi  27689  lnopmi  28037  adjlnop  28123  matunitlindflem2  32370  poimirlem4  32377  heicant  32408  mblfinlem2  32411  ismblfin  32414  ftc1anclem6  32454  ftc1anclem7  32455  ftc1anc  32457