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 394

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 395

This theorem is referenced by:  3impdi  1347  dff13  7263  f1oiso  7356  omord2  8586  fodomacn  10079  ltapi  10926  ltmpi  10927  axpre-ltadd  11190  faclbnd  14281  pwsdiagmhm  18787  tgcl  22902  brbtwn2  28772  grpoinvf  30398  ocorth  31157  fh1  31484  fh2  31485  spansncvi  31518  lnopmi  31866  adjlnop  31952  matunitlindflem2  37160  poimirlem4  37167  heicant  37198  mblfinlem2  37201  ismblfin  37204  ftc1anclem6  37241  ftc1anclem7  37242  ftc1anc  37244