Theorem anandis 679

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 661	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) → 𝜏)
3	2	anabsan 666	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  1352  dff13  7202  f1oiso  7299  omord2  8496  fodomacn  9970  ltapi  10818  ltmpi  10819  axpre-ltadd  11082  faclbnd  14217  pwsdiagmhm  18760  tgcl  22917  brbtwn2  28961  grpoinvf  30590  ocorth  31349  fh1  31676  fh2  31677  spansncvi  31710  lnopmi  32058  adjlnop  32144  matunitlindflem2  37789  poimirlem4  37796  heicant  37827  mblfinlem2  37830  ismblfin  37833  ftc1anclem6  37870  ftc1anclem7  37871  ftc1anc  37873