Theorem anandis 890

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 886	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) → 𝜏)
3	2	anabsan 871	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 197  df-an 385

This theorem is referenced by:  3impdi  1421  dff13  6552  f1oiso  6641  omord2  7692  fodomacn  8917  ltapi  9763  ltmpi  9764  axpre-ltadd  10026  faclbnd  13117  pwsdiagmhm  17416  tgcl  20821  brbtwn2  25830  grpoinvf  27514  ocorth  28278  fh1  28605  fh2  28606  spansncvi  28639  lnopmi  28987  adjlnop  29073  matunitlindflem2  33536  poimirlem4  33543  heicant  33574  mblfinlem2  33577  ismblfin  33580  ftc1anclem6  33620  ftc1anclem7  33621  ftc1anc  33623