Theorem anandis 677

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 659	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) → 𝜏)
3	2	anabsan 664	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  7292  f1oiso  7387  omord2  8623  fodomacn  10125  ltapi  10972  ltmpi  10973  axpre-ltadd  11236  faclbnd  14339  pwsdiagmhm  18866  tgcl  22997  brbtwn2  28938  grpoinvf  30564  ocorth  31323  fh1  31650  fh2  31651  spansncvi  31684  lnopmi  32032  adjlnop  32118  matunitlindflem2  37577  poimirlem4  37584  heicant  37615  mblfinlem2  37618  ismblfin  37621  ftc1anclem6  37658  ftc1anclem7  37659  ftc1anc  37661