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 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜏)

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

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 401

This theorem is used by:  3impdi  1368  dff13  7252  f1oiso  7349  omord2  8550  fodomacn  10047  ltapi  10894  ltmpi  10895  axpre-ltadd  11158  faclbnd  14333  pwsdiagmhm  18896  tgcl  23137  brbtwn2  29266  grpoinvf  30895  ocorth  31654  fh1  31981  fh2  31982  spansncvi  32015  lnopmi  32363  adjlnop  32449  matunitlindflem2  38296  poimirlem4  38303  heicant  38334  mblfinlem2  38337  ismblfin  38340  ftc1anclem6  38377  ftc1anclem7  38378  ftc1anc  38380