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 396

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 397

This theorem is referenced by:  3impdi  1350  dff13  7256  f1oiso  7350  omord2  8569  fodomacn  10053  ltapi  10900  ltmpi  10901  axpre-ltadd  11164  faclbnd  14254  pwsdiagmhm  18748  tgcl  22692  brbtwn2  28418  grpoinvf  30040  ocorth  30799  fh1  31126  fh2  31127  spansncvi  31160  lnopmi  31508  adjlnop  31594  matunitlindflem2  36788  poimirlem4  36795  heicant  36826  mblfinlem2  36829  ismblfin  36832  ftc1anclem6  36869  ftc1anclem7  36870  ftc1anc  36872