Theorem anandis 677

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 659	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) → 𝜏)
3	2	anabsan 664	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  3impdi  1347  dff13  7005  f1oiso  7098  omord2  8203  fodomacn  9516  ltapi  10363  ltmpi  10364  axpre-ltadd  10627  faclbnd  13700  pwsdiagmhm  18061  tgcl  21669  brbtwn2  26798  grpoinvf  28414  ocorth  29173  fh1  29500  fh2  29501  spansncvi  29534  lnopmi  29882  adjlnop  29968  matunitlindflem2  35334  poimirlem4  35341  heicant  35372  mblfinlem2  35375  ismblfin  35378  ftc1anclem6  35415  ftc1anclem7  35416  ftc1anc  35418