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  7254  f1oiso  7355  omord2  8557  fodomacn  10062  ltapi  10915  ltmpi  10916  axpre-ltadd  11179  faclbnd  14356  pwsdiagmhm  18944  matunitlindflem2  22906  tgcl  23198  brbtwn2  29363  grpoinvf  31014  ocorth  31773  fh1  32100  fh2  32101  spansncvi  32134  lnopmi  32482  adjlnop  32568  poimirlem4  38375  heicant  38406  mblfinlem2  38409  ismblfin  38412  ftc1anclem6  38449  ftc1anclem7  38450  ftc1anc  38452