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  7246  f1oiso  7347  onelfvnef1  8427  omord2  8553  fodomacn  10107  ltapi  10960  ltmpi  10961  axpre-ltadd  11224  faclbnd  14402  pwsdiagmhm  18989  matunitlindflem2  22957  tgcl  23249  brbtwn2  29417  grpoinvf  31068  ocorth  31827  fh1  32154  fh2  32155  spansncvi  32188  lnopmi  32536  adjlnop  32622  poimirlem4  38462  heicant  38493  mblfinlem2  38496  ismblfin  38499  ftc1anclem6  38536  ftc1anclem7  38537  ftc1anc  38539