Theorem anandis 677

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

This theorem is referenced by:  3impdi  1351  dff13  7254  f1oiso  7348  omord2  8567  fodomacn  10051  ltapi  10898  ltmpi  10899  axpre-ltadd  11162  faclbnd  14250  pwsdiagmhm  18712  tgcl  22472  brbtwn2  28194  grpoinvf  29816  ocorth  30575  fh1  30902  fh2  30903  spansncvi  30936  lnopmi  31284  adjlnop  31370  matunitlindflem2  36533  poimirlem4  36540  heicant  36571  mblfinlem2  36574  ismblfin  36577  ftc1anclem6  36614  ftc1anclem7  36615  ftc1anc  36617