Theorem anandis 678

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 660	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) → 𝜏)
3	2	anabsan 665	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  1351  dff13  7232  f1oiso  7329  omord2  8534  fodomacn  10016  ltapi  10863  ltmpi  10864  axpre-ltadd  11127  faclbnd  14262  pwsdiagmhm  18765  tgcl  22863  brbtwn2  28839  grpoinvf  30468  ocorth  31227  fh1  31554  fh2  31555  spansncvi  31588  lnopmi  31936  adjlnop  32022  matunitlindflem2  37618  poimirlem4  37625  heicant  37656  mblfinlem2  37659  ismblfin  37662  ftc1anclem6  37699  ftc1anclem7  37700  ftc1anc  37702