Theorem anandis 691

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 673	. 2 ⊢ (((𝜑 ∧ 𝜑) ∧ (𝜓 ∧ 𝜒)) → 𝜏)
3	2	anabsan 678	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜏)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  3impdi  1369  dff13  7281  f1oiso  7382  onelfvnef1  8477  omord2  8603  fodomacn  10162  ltapi  11015  ltmpi  11016  axpre-ltadd  11279  faclbnd  14461  pwsdiagmhm  19056  matunitlindflem2  23025  tgcl  23317  brbtwn2  29513  grpoinvf  31164  ocorth  31923  fh1  32250  fh2  32251  spansncvi  32284  lnopmi  32632  adjlnop  32718  poimirlem4  38734  heicant  38765  mblfinlem2  38768  ismblfin  38771  ftc1anclem6  38808  ftc1anclem7  38809  ftc1anc  38811