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  1350  dff13  7258  f1oiso  7354  omord2  8588  fodomacn  10079  ltapi  10926  ltmpi  10927  axpre-ltadd  11190  faclbnd  14312  pwsdiagmhm  18818  tgcl  22942  brbtwn2  28869  grpoinvf  30498  ocorth  31257  fh1  31584  fh2  31585  spansncvi  31618  lnopmi  31966  adjlnop  32052  matunitlindflem2  37565  poimirlem4  37572  heicant  37603  mblfinlem2  37606  ismblfin  37609  ftc1anclem6  37646  ftc1anclem7  37647  ftc1anc  37649