Theorem anandis 690

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 672	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) → 𝜏)
3	2	anabsan 677	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  3impdi  1367  dff13  7242  f1oiso  7339  omord2  8540  fodomacn  10028  ltapi  10876  ltmpi  10877  axpre-ltadd  11140  faclbnd  14317  pwsdiagmhm  18880  tgcl  23087  brbtwn2  29164  grpoinvf  30793  ocorth  31552  fh1  31879  fh2  31880  spansncvi  31913  lnopmi  32261  adjlnop  32347  matunitlindflem2  38128  poimirlem4  38135  heicant  38166  mblfinlem2  38169  ismblfin  38172  ftc1anclem6  38209  ftc1anclem7  38210  ftc1anc  38212