Theorem anandis 691

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  3impdi  1369  dff13  7258  f1oiso  7359  onelfvnef1  8450  omord2  8576  fodomacn  10136  ltapi  10989  ltmpi  10990  axpre-ltadd  11253  faclbnd  14435  pwsdiagmhm  19028  matunitlindflem2  22996  tgcl  23288  brbtwn2  29484  grpoinvf  31135  ocorth  31894  fh1  32221  fh2  32222  spansncvi  32255  lnopmi  32603  adjlnop  32689  poimirlem4  38618  heicant  38649  mblfinlem2  38652  ismblfin  38655  ftc1anclem6  38692  ftc1anclem7  38693  ftc1anc  38695