Theorem anandis 675

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

This theorem is referenced by:  3impdi  1349  dff13  7257  f1oiso  7351  omord2  8573  fodomacn  10057  ltapi  10904  ltmpi  10905  axpre-ltadd  11168  faclbnd  14257  pwsdiagmhm  18751  tgcl  22705  brbtwn2  28445  grpoinvf  30067  ocorth  30826  fh1  31153  fh2  31154  spansncvi  31187  lnopmi  31535  adjlnop  31621  matunitlindflem2  36801  poimirlem4  36808  heicant  36839  mblfinlem2  36842  ismblfin  36845  ftc1anclem6  36882  ftc1anclem7  36883  ftc1anc  36885