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  7209  f1oiso  7306  omord2  8502  fodomacn  9978  ltapi  10826  ltmpi  10827  axpre-ltadd  11090  faclbnd  14252  pwsdiagmhm  18799  tgcl  22934  brbtwn2  28974  grpoinvf  30603  ocorth  31362  fh1  31689  fh2  31690  spansncvi  31723  lnopmi  32071  adjlnop  32157  matunitlindflem2  37938  poimirlem4  37945  heicant  37976  mblfinlem2  37979  ismblfin  37982  ftc1anclem6  38019  ftc1anclem7  38020  ftc1anc  38022