Theorem anandis 685

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 667	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) → 𝜏)
3	2	anabsan 672	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 209  df-an 398

This theorem is referenced by:  3impdi  1358  dff13  7201  f1oiso  7298  omord2  8496  fodomacn  9973  ltapi  10822  ltmpi  10823  axpre-ltadd  11086  faclbnd  14247  pwsdiagmhm  18794  tgcl  22955  brbtwn2  28994  grpoinvf  30623  ocorth  31382  fh1  31709  fh2  31710  spansncvi  31743  lnopmi  32091  adjlnop  32177  matunitlindflem2  37997  poimirlem4  38004  heicant  38035  mblfinlem2  38038  ismblfin  38041  ftc1anclem6  38078  ftc1anclem7  38079  ftc1anc  38081