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  7200  f1oiso  7297  omord2  8493  fodomacn  9967  ltapi  10815  ltmpi  10816  axpre-ltadd  11079  faclbnd  14241  pwsdiagmhm  18788  tgcl  22943  brbtwn2  28993  grpoinvf  30623  ocorth  31382  fh1  31709  fh2  31710  spansncvi  31743  lnopmi  32091  adjlnop  32177  matunitlindflem2  37949  poimirlem4  37956  heicant  37987  mblfinlem2  37990  ismblfin  37993  ftc1anclem6  38030  ftc1anclem7  38031  ftc1anc  38033