Theorem anandis 678

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 660	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) → 𝜏)
3	2	anabsan 665	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 207  df-an 396

This theorem is referenced by:  3impdi  1351  dff13  7195  f1oiso  7292  omord2  8492  fodomacn  9969  ltapi  10816  ltmpi  10817  axpre-ltadd  11080  faclbnd  14215  pwsdiagmhm  18723  tgcl  22872  brbtwn2  28868  grpoinvf  30494  ocorth  31253  fh1  31580  fh2  31581  spansncvi  31614  lnopmi  31962  adjlnop  32048  matunitlindflem2  37596  poimirlem4  37603  heicant  37634  mblfinlem2  37637  ismblfin  37640  ftc1anclem6  37677  ftc1anclem7  37678  ftc1anc  37680