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  7210  f1oiso  7307  omord2  8504  fodomacn  9978  ltapi  10826  ltmpi  10827  axpre-ltadd  11090  faclbnd  14225  pwsdiagmhm  18768  tgcl  22925  brbtwn2  28990  grpoinvf  30619  ocorth  31378  fh1  31705  fh2  31706  spansncvi  31739  lnopmi  32087  adjlnop  32173  matunitlindflem2  37857  poimirlem4  37864  heicant  37895  mblfinlem2  37898  ismblfin  37901  ftc1anclem6  37938  ftc1anclem7  37939  ftc1anc  37941