Theorem anandis 690

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  3impdi  1367  dff13  7252  f1oiso  7349  omord2  8551  fodomacn  10039  ltapi  10887  ltmpi  10888  axpre-ltadd  11151  faclbnd  14326  pwsdiagmhm  18889  tgcl  23105  brbtwn2  29221  grpoinvf  30850  ocorth  31609  fh1  31936  fh2  31937  spansncvi  31970  lnopmi  32318  adjlnop  32404  matunitlindflem2  38234  poimirlem4  38241  heicant  38272  mblfinlem2  38275  ismblfin  38278  ftc1anclem6  38315  ftc1anclem7  38316  ftc1anc  38318