Theorem anandis 674

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

Syntax hints:   → wi 4   ∧ wa 395

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 396

This theorem is referenced by:  3impdi  1348  dff13  7122  f1oiso  7215  omord2  8374  fodomacn  9796  ltapi  10643  ltmpi  10644  axpre-ltadd  10907  faclbnd  13985  pwsdiagmhm  18450  tgcl  22100  brbtwn2  27254  grpoinvf  28873  ocorth  29632  fh1  29959  fh2  29960  spansncvi  29993  lnopmi  30341  adjlnop  30427  matunitlindflem2  35753  poimirlem4  35760  heicant  35791  mblfinlem2  35794  ismblfin  35797  ftc1anclem6  35834  ftc1anclem7  35835  ftc1anc  35837